\begin{slide}{CDCL: Spezifikation}

conflict driven clause learning 
\begin{itemize}\itemsep 2pt
\item wenn (nach Unit-Propagation) ein Konflikt
  auftritt,
\item dann wird eine neue Klausel $C'$ berechnet 
  (\glqq gelernt\grqq) und zur Formel $F$ hinzugefügt
\item  sowie ein früherer Entscheidungspunkt $p$
  als Ziel für Backjump bestimmt.
\item so daß $F \models C'$, d. h. die Bedeutung
  wird nicht geändert,
\item und $C'$ in $p$ sofort eine Unit-Propagation
  bewirkt
\end{itemize}

\end{slide}
