How to adapt DPLL to solve HORNSAT? 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)$:


IF $S = \emptyset $ RET SAT
WHILE $\exists$ one unit clause $(p)$ or $\exists$ one literal $p$ that appears pure in $S$ 
IF ( $p \in S \wedge \neg p \in S) $ RET UNSAT
ELSE $S = Unit-propagate(S,p)$ 
ENDIF ENDWHILE
IF $S = \emptyset $ RET SAT
choose one literal $p$ in one clause in $S$
IF $(DPLL(Unit-propagate(S,p) == SAT)$ RET SAT
ELSE RET $DPLL(Unit-propagate(S,\neg p)$ 


FUNCTION $Unit-propagate(S,p)$


Delete every clause in $s$ that contains $p$
Delete every occurence of $\neg p$
RET $S$
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.