
\begin{slide}{Algorithmen für FD-Solver}
DPLL für SAT:
\begin{itemize}\itemsep 2pt\parskip 2pt
\item Zustand (Knoten im Suchbaum) ist partielle Belegung
 \item Schritte (Kanten): Decide, Propagate, Conflict, Backtrack
\end{itemize}
grundsätzliches Vorgehen bei FD:
\begin{itemize}\itemsep 2pt\parskip 2pt
\item Zustand ist \emph{Bereichs-Abbildung}: $\dom: V \to 2^U$

\item Decide: wähle $d\in \dom(v)$, Kind-Knoten $\dom'(v)=\{d\}$
\item Backtrack: wähle ein anderes $d'\in\dom(v)$
\item Conflict: $\dom$ fehlgeschlagen 
\item Propagate: verkleinere die Domains von Variablen

(schließe Werte aus, die zu Inkonsistenzen führen)

dafür gibt es (im Unterschied zu DPLL) viele Varianten
\end{itemize}


\end{slide}
