\begin{slide}{Beispiele zur SAT-Modellierung}

  \begin{itemize}\itemsep 0pt\parskip 0pt
  \item Hausaufgabe (leicht): $N$-Damen-Problem 
  \item Hausaufgabe (schwer): Rösselsprung ($=$ Hamiltonkreis)
  \item von $n$ Variablen sind genau $k$ wahr
    (bei Formelgröße $\sim n\cdot k$)
  \item Puzzles aus \emph{Logisch} (Dt. Rätselverlag)
  \item Puzzles von \url{http://www.janko.at/}
  \end{itemize}

Vorgehen bei Modellierung:
\begin{itemize}\itemsep 2pt\parskip 2pt
\item welches sind die Variablen, was ist deren Bedeutung?

  (Wie rekonstruiert man eine Lösung
  aus der Belegung, die der Solver liefert?)
\item welches sind die Constraints?\\
 wie stellt man sie in CNF dar?
\end{itemize}

\end{slide}
