
\begin{slide}{DPLL/CDCL (Implementierung, Übung)}

(Kroening/Strichman Abschn. 2.2.4)

\begin{verbatim}
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);     
\end{verbatim}

Beispiel: $-1 \vee 2, -1\vee 3\vee 5, -2\vee 4,
-3 \vee -4, 1\vee 5\vee -2, 2\vee 3,2\vee -3,
6\vee -5,\dots$. (weitere Klauseln mit anderen Var.)

Entscheidungen: $\dots,-6,\dots,1$. 
Welche Klausel wird gelernt?
Zu welchem Punkt wird zurückgekehrt?

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

\end{slide}

