This is an old revision of the document!
Polynomial Algorithm for Horn Clauses
A Horn clause is a clause that has at most one positive literal.
Such clause is either of the form where
is a variable, or of the form
for
, that is
.
The following algorithm eliminates clauses of the form , keeping only clauses that have at least one assumption.
To check satisfiability of a set of Horn clauses:
- while the set contains a clause of the form
where
is a propositional variable:
- erase all clauses that contain literal
- remove
from all literals
- if there is an empty clause, set is not satisfiable
- if no contradiction found, the set is satisfiable
On we conclude that
must be true and derive valid consequences of this fact. If we obtain contradiction, the set of clearly unsatisfiable.
Moreover, if loop terminates then every clause contains a negative literal. The assignment that sets all remaining variables to false is a satisfying assignment.