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$