DPLL-Algorithmus

Eingabe: CNF F,
Ausgabe: Belegung b mit b $\models$ F oder UNSAT.

DPLL(b)     (verwendet Keller für Entscheidungspunkte):

• (success) falls b $\models$ F, dann Ausgabe b und halt.
• (backtrack) falls F eine b-Konfliktklausel enthält, dann:
  • falls Keller leer, dann Ausgabe UNSAT und halt.
  • sonst v : = pop() und DPLL(b_{< v}∪{(v, 1)}.
  dabei ist b_{< v} die Belegung vor decide(v)
• (propagate) falls F eine b-Unitklausel l enthält: DPLL(b∪{(l, 1)}).
• (decide) sonst wähle v $\notin$domb, push(v), und DPLL(b∪{(v, 0)}).