HORN-SATISFIABILITY

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 $$
eg l 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 $$
eg l. Horn satisfiability is actually one of the "hardest" or "most expressive" problems which can be computed 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]

Contents

See also

References

See also

★ Unit propagation

★ Boolean satisfiability problem

★ 2-satisfiability

References

1.
On renamable Horn and generalized Horn functions, , Vijaya, Chandru, Annals of Mathematics and Artificial Intelligence, 2005