\begin{slide}{Lösung von Differenz-Constraints}

  \begin{itemize}
  \item 
(später:) Boolesche Kombinationen
werden durch DPLL(T) behandelt,
\item
(jetzt:) der Theorie-Löser behandelt Konjunktionen
von Differenz-Konstraints.
\item
  deren Lösbarkeit ist in Polynomialzeit entscheidbar,
\item
Hilfsmittel: Graphentheorie (kürzeste Wege),
  schon lange bekannt (Bellman 1958, Ford 1960),
\end{itemize}

\end{slide}
