# 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.

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)$

1. Delete every clause in $s$ that contains $p$
2. Delete every occurence of $\neg p$
3. RET $S$