Algorithm DPLL (clauses)
1. If clauses is empty clause set, Succeed
2. If clauses contains an empty clause, Fail
3. If clauses contains a unit clause (literal)
- return result of DPLL(clauses[literal])
- clauses[literal] means simplify clauses with value of literal
4. Else heuristically choose a variable u
- heuristically choose a value v
- 4.a. If DPLL(clauses[u:=v]) succeeds, Succeed
- 4.b. Else return result of DPLL(clauses[u:= not v])