How to adapt DPLL to solve HORNSAT?

Question

This question wask asked in a homework of Computer Theory in Rome, Italy.

How to simplify the DPLL algorithm in order to solve HORNSAT?

My Approach:

I know that an Horn clause is an OR of literals where it contains at most one pure literal and any number of negative literals.

I would start with the following algorithm:

FUNCTION $Dpll(S)$:

1. IF $S = \emptyset $ RET SAT
2. WHILE $\exists$ one unit clause $(p)$ or $\exists$ one literal $p$ that appears pure in $S$
3. IF ( $p \in S \wedge \neg p \in S) $ RET UNSAT
4. ELSE $S = Unit-propagate(S,p)$
5. ENDIF ENDWHILE
6. IF $S = \emptyset $ RET SAT
7. choose one literal $p$ in one clause in $S$
8. IF $(DPLL(Unit-propagate(S,p) == SAT)$ RET SAT
9. ELSE RET $DPLL(Unit-propagate(S,\neg p)$

FUNCTION $Unit-propagate(S,p)$

10. Delete every clause in $s$ that contains $p$
11. Delete every occurence of $\neg p$
12. RET $S$

Answer 1

Horn formulas are always satisfiable unless there is at least one unit clause that contains a positive literal. (Otherwise assigning false to all the variables guarantees the formula would be satisfied.) The procedure in that case is to unit propagate all unit clauses that contain a positive literal and unit propagate any such new clauses as they occur. Once this task is completed, if the remaining formula contains no empty clauses then the Horn formula is satisfiable.