\begin{slide}{FD und SAT}

  \begin{itemize}\itemsep 2pt \parskip 2pt
  \item für alle konsistenz-basierten Methoden gilt

    wenn man nichts mehr propagieren kann, 
    muß man entscheiden
  \item dabei wählt man einen aus evtl. sehr vielen Werten,
    d.h. man muß später oft zurückkehren (backtrack)
  \item
    man könnte sich zunächst nur für die linke oder rechte
    Hälfte eines Intervalls entscheiden (dann nur ein Backtrack)
  \item
    das entspricht einer Binärdarstellung 
  
    dann kann man gleich ein aussagenlogisches Constraintsystem
    benutzen: der Löser kann dann Klauseln lernen usw.
  \end{itemize}


\end{slide}
