\begin{slide}{Themen zum Weiterarbeiten}

\begin{itemize} \itemsep 3pt\parskip 2pt
\item optimierte SAT-Kodierung für 
  binäre Addition, Multiplikation
\item Optimierung von Parametern für
  Constraint-Solver (innerhalb eines
  Terminationsbeweisers)
\item \glqq didaktisch wertvolle\grqq\ 
  Implementierungen (d. h. in Haskell)
  wichtiger Algorithmen (DPLL, CDCL, 
  Fourier-Motzkin, DPLL(T))
\item \dots und daraus abgeleitete autotool-Aufgaben
\item Verbesserung von satchmo-smt (bitblasting SMT solver)
\item SAT-Kodierungen 
  in der Bioinformatik (RNA folding)
\item SAT-Kodierungen für Zweipersonen(end)spiele
\item SAT-Solver   auf (hoch)paralleler Hardware
\end{itemize}

\end{slide}
