Horn-satisfiability
From Wikipedia, the free encyclopedia
In formal logic, Horn-satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable.
A Horn clause is a clause with at most one positive literal, called the head of the clause, and any number of negative literals, forming the body of the clause. A Horn formula is a propositional formula formed by conjunction of Horn clauses.
The problem of Horn satisfiability is solvable in polynomial time. A polynomial-time algorithm for Horn satisfiability is based on the rule of unit propagation: if the formula contains a clause composed of a single literal l (a unit clause), then all clauses containing l are removed, and all clauses containing 
have this literal removed. The result of the second rule may itself be a unit clause, which is propagated in the same manner. The formula is satisfiable if this transformation does not generate a pair of opposite unit clauses l and . Horn satisfiability is actually one of the "hardest" or "most expressive" problems which is known to be computable in polynomial time, in the sense that it is a P-complete problem.
This algorithm also allows determining a truth assignment of satisfiable Horn formulae: all variables contained in a unit clause are set to the value satisfying that unit clause; all other literals are set to false. The resulting assignment is the minimal model of the Horn formula, that is, the assignment having a minimal set of variables assigned to true, where comparison is made using set containment.
Using a linear algorithm for unit propagation, the algorithm is linear in the size of the formula.
It is logical to wonder if Horn-SAT can be used to prove that P=NP, by converting any SAT problem to a Horn-SAT problem and then solving it in polynomial time. The problem with this is two-fold. First, transforming a SAT problem to a Horn-SAT problem takes exponential time. Second, the resultant transformation is exponential in length.
A generalization of the class of Horn formulae is that of renamable-Horn formulae, which is the set of formulae that can be placed in Horn form by replacing some variables with their respective negation. Checking the existence of such a replacement can be done in linear time; therefore, the satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula.[1]
