\begin{slide}{DPLL(T)}

Ansatz:
für jede elementare Formel $F = P(t_1,\ldots,t_k)$ \\
eine neue boolesche Unbekannte $p_F \leftrightarrow F$, \\ 
dann SAT-Problem für die $p_*$ lösen.

Ideen:
\begin{itemize}
\item naiv (SAT): belegen, testen, backtrack.
\item DPLL (SAT): 
  partiell belegen, t., b., propagieren (, lernen)
\item DPLL(T) (SMT): 
  Test in Theorie $T$, Theorie-Propagation.
\end{itemize}
(optimized lazy approach)

\bigskip

Übersichtsvortrag: Robert Nievenhuis et al.
\url{http://www.lsi.upc.edu/~roberto/RTA07-slides.pdf}

\end{slide}

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

T $=$ LRA (linear real arithmetic)

durch Tseitin-Transformation
als CNF darstellen (zusätzliche boolesche Variablen)

DPLL(T) benutzt
\begin{itemize}
\item T-Solver 
  für Konjunktion von vollst. belegten Klauseln

  (z. B. Simplexverfahren)
\item T-Propagation 

  (z. B. $x\le y \wedge y\le z \Rightarrow x\le z$)
\item T-Lerner

  bei Nichterfüllbarkeit liefert T-Solver
  eine \glqq Begründung\grqq\ 
  (kleine nicht erfüllbare Teilmenge)
\end{itemize}

\end{slide}
