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


\begin{itemize} \itemsep 2pt
\item T-Solver 
  für Konjunktion von Atomen

  z. B. Simplex, Fourier-Motzkin
\item T-Konfliktanalyse:
  
  bei Nichterfüllbarkeit liefert T-Solver
  eine \glqq Begründung\grqq\ 

  $=$ (kleine) nicht erfüllbare Teilmenge (von Atomen $\{a_1,\ldots,a_k\}$),
  dann Klausel $\neg a_1\vee \ldots\vee \neg a_k$ lernen

\item T-Deduktion, Bsp: aus $x\le y \wedge y\le z$  folgt  $x\le z$ 

  neues (!) Atom $x\le z$ entsteht durch Umformungen während Simplex 
  oder Fourier-Motzkin

  betrachte $\neg x\le y \vee \neg y\le z \vee x\le z$
  als Konfliktklausel, damit CDCL
\end{itemize}

\end{slide}
