DPLL mit CDCL (Plan)

conflict driven clause learning, Lernen von Konfliktklauseln

bei jedem Konflikt:

• (minimale) Ursache (d. h. partielle Belegung) feststellen
• Negation der Konfliktursache als neue Klausel K hinzufügen

Eigenschaften:

• danach backjump zur vorletzten Variable in K.

  (die letzte Variable wird dann propagiert, das ergibt die richtige Fortsetzung der Suche)

• K führt auch später zu Propagationen, d.h. Verkürzung der Suche