On renamable horn and generalized horn functions

A Boolean function in disjunctive normal form (DNF) is aHorn function if each of its elementary conjunctions involves at most one complemented variable. Ageneralized Horn function is constructed from a Horn function by disjuncting a nested set of complemented variables to it. The satisfiability problem is solvable in polynomial time for both Horn and generalized Horn functions. A Boolean function in DNF is said to berenamable Horn if it is Horn after complementation of some variables. Succinct mathematical characterizations and linear-time algorithms for recognizing renamable Horn and generalized Horn functions are given in this paper. The algorithm for recognizing renamable Horn functions gives a new method to test 2-SAT. Some computational results are also given