
\begin{slide}{Überblick}

Spezifikation:
\begin{itemize}\itemsep 2pt
\item Eingabe: eine Formel in CNF
\item Ausgabe: 
  \begin{itemize}\itemsep 2pt
  \item eine erfüllende Belegung
  \item \emph{oder} ein Beweis für Nichterfüllbarkeit
  \end{itemize}
\end{itemize}
Verfahren:
\begin{itemize}\itemsep 2pt
\item evolutionär (Genotyp $=$ Belegung)
\item lokale Suche (Walksat)
\item DPLL (Davis, Putnam, Logeman, Loveland)
\end{itemize}

\end{slide}
