\begin{slide}{SAT als IP}

gesucht ist Funktion $T : \text{CNF} \to \text{IP}$ mit
\begin{itemize}
\item $T$ ist in Polynomialzeit berechenbar
\item $\forall F\in \text{CNF} : F ~ \text{erfüllbar} \iff T(F) ~ \text{lösbar}$
\end{itemize}

Lösungsidee:
\begin{itemize}
\item Variablen von $T(F)$ $=$ Variablen von $F$
\item Wertebereich der Variablen ist $\{0,1\}$
\item Negation durch Subtraktion, Oder durch Addition, Wahrheit durch $\ge 1$
\end{itemize}

\end{slide}
