\begin{slide}{Algorithmen für FD-Solver (Ansatz)}

zum Lösen eines Constraint-Systems $F$: --- DPLL für SAT:
\begin{itemize}\itemsep 0pt\parskip 2pt
\item Zustand (Knoten im Suchbaum) ist partielle Belegung $b$
\item Def.: $b_1\le b_2$ falls $b_1\supseteq b_2$,

  $(F,b)$ ist \emph{konsistent} (erfüllbar): $\exists b'\le b: b'\models F$
\item Invariante: 

  für jeden Knoten $b$ mit Kindern $b_1 (,b_2)$ gilt: $b_i\le b$ und

  ($(F,b)$ konsistent $\iff$ $b\models F \vee \exists i:$ $(F,b_i)$ konsistent)
\end{itemize}
grundsätzliches Vorgehen bei FD:
\begin{itemize}\itemsep 0pt\parskip 2pt
\item Zustand ist \emph{Bereichs-Abbildung}: $\dom: V \to 2^U$

  ordnet jeder Variablen eine Teilmenge (\emph{domain}) von $U$ zu
\item Inv.: für $\dom$ mit Kindern $\dom_1,\ldots$ gilt:
  $\dom_i\le \dom$ und

  ($(F,\dom)$ kons.
  $\Leftrightarrow$ $(F,\dom)$ gelöst $\vee\exists i:$ $(F,\dom_i)$ kons.).

\end{itemize}

\end{slide}
