\begin{slide}{Kernthemen}

Aussagenlogik (SAT)
\begin{itemize}\itemsep 0pt
\item Grundlagen: Formeln, BDDs, Resolution, DPLL, CDCL
\item Anwendungen: SAT-Kodierungen für
  kombinatorische Aufgaben, Bit-Blasting
  für andere Constraint-Bereiche
\end{itemize}
Prädikatenlogik: Bereiche und -spezifische Verfahren:
\begin{itemize}\itemsep 0pt
\item Zahlen: lineare Gleichungen,
  lineare Ungleichungen, Polynome, 
  Presburger-Arithmetik
\item uninterpretierte Funktionen, Arrays
\end{itemize}
Prädikatenlogik: allgemeine Verfahren:
\begin{itemize}\itemsep 0pt
\item Kombinationen von Theorien (Nelson-Oppen)
\item Kombination von Theorie und SAT (DPLL(T))
\end{itemize}

\end{slide}
