DPLL

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

Zustand = mathend000# partielle Belegung

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

  Beispiel: Klausel x₁∨x₃ mathend000#, partielle Belegung x₁ = 0 mathend000#,

  Folgerung: x₃ = 1 mathend000#

• bei Konflikt (widersprüchliche Folgerungen)
  • Backtrack (zu letztem Decide)
  • Backjump (zu früherem Decide)