\begin{slide}{Benutzung von SAT-Solvern}

Eingabeformat: SAT-Problem in CNF:
\begin{itemize}\itemsep 0pt\parskip 0pt
\item Variable $=$ positive natürliche Zahl
\item Literal $=$ ganze Zahl ($\neq 0$, mit Vorzeichen)
\item Klausel $=$ Zeile, abgeschlossen durch $0$.
\item Programm $=$ Header \verb|p cnf <#Variablen> <#Klauseln>|,
  dann Klauseln
\end{itemize}
Beispiel
\begin{verbatim}
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0
\end{verbatim}
Löser:
\verb|minisat input.cnf output.text|


\end{slide}
