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.
To check satisfiability of a set of Horn clauses:
- set initially all variables to false
- 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