DPLL

Davis, Putnam (1960), Logeman, Loveland (1962), http://dx.doi.org/10.1145/321033.321034http://dx.doi.org/10.1145/368273.368557

Zustand = partielle Belegung

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

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

  Folgerung: x₃ = 1

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