DPLL

Davis, Putnam (1960), Logeman, Loveland (1962)

Zustand = partielle Belegung

• Decide: eine Variable belegen
• Propagate: alle Schlußfolgerungen ziehen

  Beispiel: Klausel x₁ $\vee$ x₃, Belegung x₁ = 0, Folgerung: x₃ = 1

• bei Konflikt: Backtrack/Backjump