Horn Clause Solver Lab

Horn clause: a CNF clause with at most one positive literal.  ·  Types: fact single positive (p)  ·  rule one positive + negatives (-a ∨ -b ∨ c)  ·  goal all negatives (-a ∨ -b)
Algorithm: while ∃ unit positive clause (p) → set p=TRUE · remove satisfied clauses · simplify (remove ¬p) · check for empty clause → UNSAT. When no more unit positives remain → SAT.