bei DPLL für CNF F: bei Konflikt für Variable k
mit aktueller Belegung b
bestimme Konflikt-Graph
Konflikt-Ursache: die Menge der Decide-Knoten,
von denen aus die Konfliktvariable erreichbar ist.
gelernte Klausel:
(¬b(v1)∨…¬b(vn),
wobei
{v1,…, vn} die Konfliktursache ist
Satz: diese Klausel K folgt aus der Formel F
...d.h. Mod(F) = Mod(F∪{K})