\begin{slide}{DPLL mit CDCL (Plan)}
conflict driven clause learning,
Lernen von Konfliktklauseln

  bei jedem Konflikt:
  \begin{itemize}\itemsep 0pt\parskip2pt
  \item (minimale) Ursache 
    (d. h. partielle Belegung) feststellen
  \item Negation der Konfliktursache
    als neue Klausel $K$ hinzufügen
  \end{itemize}
Eigenschaften:
\begin{itemize}
\item danach \emph{backjump} 
  zur vorletzten Variable in $K$.
  
  (die letzte Variable wird dann propagiert, 
  das ergibt die richtige Fortsetzung der Suche)
\item $K$ führt auch später  zu
  Propagationen, d.h. Verkürzung der Suche
\end{itemize}


\end{slide}

\begin{slide}{DPLL mit CDCL (Einzelheiten)}

bei DPLL für CNF $F$: bei Konflikt für Variable $k$ \\
mit aktueller Belegung $b$
bestimme \emph{Konflikt-Graph}
\begin{itemize}
\item Knoten: $\dom(b) \cup \{k\}$ 
\item Kanten: $v\to v'$, 
  falls $v$' durch eine Propagation belegt wurde
  mit einer Unit-Klausel, die $v$ enthält
\end{itemize}
(durch Decide belegten Variablen haben keine Vorgänger.)

\emph{Konflikt-Ursache}: die Menge der Decide-Knoten, \\
von denen aus die Konfliktvariable erreichbar ist.

\emph{gelernte Klausel}: 
$(\neg b(v_1)\vee \ldots \neg b(v_n)$, \\
wobei $\{v_1,\ldots,v_n\}$  die Konfliktursache ist

\emph{Satz}: diese Klausel $K$ folgt aus der Formel $F$

\dots d.h. $\Mod(F)=\Mod(F\cup\{K\})$

\end{slide}
