\begin{slide}{DPLL}

Davis, Putnam (1960), Logeman, Loveland (1962),
\begin{small}
\url{http://dx.doi.org/10.1145/321033.321034}
\url{http://dx.doi.org/10.1145/368273.368557}
\end{small}




Zustand $=$ partielle Belegung
\begin{itemize}\itemsep 2pt \parskip 2pt
\item \emph{Decide}: eine Variable belegen
\item \emph{Propagate}: alle Schlußfolgerungen ziehen

  Beispiel: Klausel $x_1\vee x_3$, 
  partielle Belegung $x_1=0$,

  Folgerung: $x_3=1$
\item bei \emph{Konflikt} (widersprüchliche
Folgerungen)
\begin{itemize}
\item (DPLL original) Backtrack (zu letztem Decide)
\item (DPLL mit CDCL) Backjump (zu früherem Decide)
\end{itemize}

\end{itemize}

\end{slide}


\begin{slide}{DPLL-Begriffe}

für partielle Belegung $b$ (Bsp: $\{(x_1,1),(x_3,0)\}$): Klausel $c$ ist
\begin{itemize} \itemsep 1pt \parskip 1pt
\item \emph{erfüllt}, 
  falls $\exists l\in c: b(l)=1$, Bsp: $(\neg x_1\vee x_2\vee \neg x_3)$
\item \emph{Konflikt},
  falls $\forall l\in c: b(l)=0$, Bsp: $(\neg x_1\vee x_3)$
\item \emph{unit},
  falls $\exists l\in c: b(l)=\bot \wedge \forall l'\in (c\setminus\{l\}): b(l')=0$,
  
  Bsp: $(\neg x_1 \vee \neg x_2 \vee x_3)$. Dabei ist $l=\neg x_2$ das Unit-Literal.
\item \emph{offen}, sonst. Bsp: $(x_2\vee x_3\vee x_4)$.
\end{itemize}

Eigenschaften: für CNF $F$ und partielle Belegung $b$:
\begin{itemize}  \itemsep 1pt \parskip 1pt
\item 
wenn $\exists c\in F$ : $c$ ist Konflikt für $b$,
dann  $\neg \exists b'\supseteq b$ mit $b'\models F$

(d.h., die Suche kann dort abgebrochen werden)
\item
wenn $\exists c\in F$: $c$ ist Unit für $b$ mit Literal $l$,
dann $\forall b'\supseteq b: b'\models F \Rightarrow b'(l)=1$

(d.h., $l$ kann ohne Suche belegt werden)
\end{itemize}

\end{slide}

\newcommand{\DPLL}{\operatorname{DPLL}}

\begin{slide}{DPLL-Algorithmus}

Eingabe: CNF $F$, \\
Ausgabe: Belegung $b$ mit $b\models F$ oder UNSAT.

$\DPLL(b)$ \quad (verwendet Keller für Entscheidungspunkte):
  \begin{itemize}  \itemsep 3pt \parskip 3pt
  \item (success) falls $b\models F$, dann Ausgabe $b$ und halt.
  \item (backtrack) falls $F$ eine $b$-Konfliktklausel enthält, dann:
    \begin{itemize}
    \item 
    falls Keller leer, dann Ausgabe UNSAT und halt.
  \item
    sonst $v := pop()$ und $\DPLL(b_{<v} \cup \{(v,1)\}$.
    \end{itemize}
    dabei ist $b_{<v}$ die Belegung \emph{vor} decide$(v)$
  \item (propagate) falls $F$ eine $b$-Unitklausel $l$  enthält: $\DPLL(b\cup\{(l,1)\})$.
  \item (decide) sonst wähle $v\notin\dom b$, push$(v)$,
    und $\DPLL(b\cup\{(v,0)\})$.
  \end{itemize}

\end{slide}

\begin{slide}{DPLL-Beispiel}

\begin{verbatim}
[[2,3],[3,5],[-3,-4],[2,-3,-4]
,[-3,4],[1,-2,-4,-5],[1,-2,4,-5]]
\end{verbatim}

decide belegt immer die kleinste freie Variable,
immer zunächst negativ  

\end{slide}

\begin{slide}{DPLL-Beispiel (Lösung)}

\begin{verbatim}
[[2,3],[3,5],[-3,-4],[2,-3,-4]
,[-3,4],[1,-2,-4,-5],[1,-2,4,-5]]

[Dec (-1),Dec (-2),Prop 3,Prop (-4),Back
,Dec 2,Dec (-3),Prop 5,Prop (-4),Back
,Dec 3,Prop (-4),Back,Back,Back
,Dec 1,Dec (-2),Prop 3,Prop (-4),Back
,Dec 2,Dec (-3),Prop 5]
\end{verbatim}
  

\end{slide}
