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