CDCL: Spezifikation

conflict driven clause learning

• wenn (nach Unit-Propagation) ein Konflikt auftritt,
• dann wird eine neue Klausel C' mathend000# berechnet („gelernt``) und zur Formel F mathend000# hinzugefügt
• sowie ein früherer Entscheidungspunkt p mathend000# als Ziel für Backjump bestimmt.
• so daß F $\models$ C' mathend000#, d. h. die Bedeutung wird nicht geändert,
• und C' mathend000# in p mathend000# sofort eine Unit-Propagation bewirkt