CDCL: Implementierung, Übung

(Kroening/Strichman Abschn. 2.2.4)

cl := aktuelle Konfliktklausel;
while (cl enthält >= 2 Literale >= aktuell)
  lit := zuletzt zugewiesenes Literal aus cl;
  var := die Variable aus lit;
  ante := die Klausel, die in der Propagation
      benutzt wurde, welche  lit  belegt hat;
  cl := Resolve (ante, cl, var);

Beispiel: -1∨2, -1∨3∨5, -2∨4, -3∨ -4, 1∨5∨ -2, 2∨3, 2∨ -3, 6∨ -5,... mathend000#. (weitere Klauseln mit anderen Var.)

Entscheidungen: ..., -6,..., 1 mathend000#. Welche Klausel wird gelernt? Zu welchem Punkt wird zurückgekehrt?

(vlg. auch Beispiel in Folien v. Nieuvenhuis.)