\begin{slide}{Gliederung der Vorlesung}

  \begin{itemize}\itemsep 1pt \parskip 1pt
  \item Aussagenlogik
    \begin{itemize}
    \item CNF-SAT-Constraints (Normalf., Tseitin-Transformation)
    \item DPLL-Solver, Backtracking und Lernen
    \item ROBDDs (Entscheidungsdiagramme)
    \end{itemize}
  \item Prädikatenlogik (konjunktive Constraints)
    \begin{itemize}
  \item Finite-Domain-Constraints
  \item naive Lösungsverfahren, Konsistenzbegriffe
  \item lineare Gleichungen, Ungleichungen, Polynomgleichungen
  \item Termgleichungen, Unifikation
    \end{itemize}
\item Kombinationen
  \begin{itemize}
  \item Kodierungen nach CNF-SAT (FD, Zahlen)
  \item SMT, DPLL(T)
  \end{itemize}
  \end{itemize}

\end{slide}
