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 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. [cite journal
last=Chandru
first=Vijaya
coauthors=Collette R. Coullard, Peter L. Hammer, Miguel Montañez, and Xiaorong Sun
title=On renamable Horn and generalized Horn functions
journal=Annals of Mathematics and Artificial Intelligence
year=2005
doi=10.1007/BF01531069
volume=1
issue=1-4
pages=33–47]

ee also

* Unit propagation
* Boolean satisfiability problem
* 2-satisfiability

References