\begin{slide}{SMT $=$ Satisfiability modulo Theory}

\begin{itemize} \itemsep 0pt
\item Aufgabenstellung:

Erfüllbarkeitsproblem 
für beliebige boolesche Kombinationen
von atomaren Formeln aus einer Theorie

Beispiel: $x\ge 3 \vee x+y\le 4 \leftrightarrow x> y$ 

\item Lösungsplan:
\begin{itemize}
\item Umformung in erfüllbarkeitsäquivalente CNF  (Tseitin)
\item Lösung durch Variante von DPLL
  (``DPLL modulo Theory'')
\end{itemize}
\end{itemize}
Literatur: Kroening/Strichman, Kap. 11

\end{slide}

