\begin{slide}{DPLL(T), Prinzip}

Ansatz:
für jedes Atom $A = P(t_1,\ldots,t_k)$ \\
eine neue boolesche Unbekannte 
$p_A \leftrightarrow A$.

naives Vorgehen:
\begin{itemize} \itemsep 2pt
\item für jede Lösung des SAT-Problem für diese Variablen $p_*$:
\item feststellen, ob die dadurch beschriebene
  Konjunktion von Atomen in der Theorie $T$ 
  erfüllbar ist
\end{itemize}

Realisierung mit DPLL(T): 
  \begin{itemize}  \itemsep 2pt
  \item decide, $T$-solve (Konjunktion von $T$-Atomen)
  \item Konflikte (logische und $T$-Konfl.): backtrack
  \item logische Propagationen, Lernen 
  \item $T$-Propagation ($T$-Deduktion)
  \end{itemize}

\end{slide}

