
\newcommand{\Var}{\operatorname{Var}}

\begin{slide}{Erfüllbarkeits-Äquivalenz}

Def: $F$ und $G$ \emph{erfüllbarkeitsäquivalent},
wenn $\Mod(F)\neq\emptyset \iff \Mod(G)\neq\emptyset$.

Satz:
es gibt einen Polynomialzeit-Algorithmus,
der zu jeder Formel $F$ 
eine erfüllbarkeitsäquivalente CNF-Formel $G$ berechnet.


\bigskip
also auch $|G| = \text{Poly}(|F|)$

\end{slide}


\begin{slide}{Tseitin-Transformation}

Gegeben $F$, gesucht erfüllbarkeitsäquivalentes $G$ in CNF.

Berechne $G$ mit $\Var(F)\subseteq\Var(G)$ und 
$\forall b: b\models F 
\iff \exists b' : b \subseteq b' \wedge b'\models G$.

Plan:
\begin{itemize}\itemsep 2pt\parskip 0pt
\item 
  für jeden nicht-Blatt-Teilbaum $T$ des Syntaxbaumes von $F$
  eine zusätzliche Variable $n_T$ einführen,
\item wobei gelten soll: $\forall b': \val(n_T,b') = \val(T,b)$.
\end{itemize}
Realisierung:
\begin{itemize}\itemsep 2pt\parskip 0pt
\item falls (Bsp.) $T=L \vee R$, 
  dann $n_T \leftrightarrow (n_L \vee n_R)$ 
  als CNF-Constraintsystem
\item jedes solche System hat $\le 8$ Klauseln mit $3$ Literalen,
  es sind ingesamt $|F|$ solche Systeme.
\end{itemize}


\end{slide}

\begin{slide}{Tseitin-Transformation (Übung)}

Übungen (Hausaufgabe):
\begin{itemize}
\item  transformiere 
$(x_1 \leftrightarrow x_2) \leftrightarrow (x_3 \leftrightarrow x_4)$
\end{itemize}
nach Tseitin-Algorithmus.




\begin{itemize}
\item Halb-Adder (2 Eingänge $x,y$, 2 Ausgänge $r,c$)

  $(r\leftrightarrow (\neg(x\leftrightarrow y)))
  \wedge (c \leftrightarrow (x\wedge y))$
\item Voll-Adder (3 Eingänge, 2 Ausgänge)


\end{itemize}


\end{slide}
