DPLL mit CDCL (Einzelheiten)

bei DPLL für CNF F: bei Konflikt für Variable k
mit aktueller Belegung b bestimme Konflikt-Graph

• Knoten: dom(b)∪{k}
• Kanten: v→v', falls v' durch eine Propagation belegt wurde mit einer Unit-Klausel, die v enthält

(durch Decide belegten Variablen haben keine Vorgänger.)

Konflikt-Ursache: die Menge der Decide-Knoten,
von denen aus die Konfliktvariable erreichbar ist.

gelernte Klausel: (¬b(v₁)∨…¬b(v_n),
wobei {v₁,…, v_n} die Konfliktursache ist

Satz: diese Klausel K folgt aus der Formel F

...d.h. Mod(F) = Mod(F∪{K})