\begin{slide}{Fourier-Motzkin für SAT?}

(Wiederholung F-M)

$\exists x : 
K_1 \le x \wedge \ldots \wedge K_p\le x
\wedge x\le G_1\wedge\ldots\wedge x\le G_q$

$\iff$ $\bigwedge_{1\le i\le p, 1\le j\le q} K_i\le G_j$

\bigskip

vergleiche mit \emph{Resolution}:
\begin{eqnarray*}
(A \vee x) \wedge (\neg x \vee B)
& \Rightarrow & (A \vee B) \\
(\neg A \to x) \wedge (x \to B)
& \Rightarrow & (\neg A \to B) \\
(\neg A \le x) \wedge (x \le B)
& \Rightarrow & (\neg A \le B)
\end{eqnarray*}

Elimination von $x$ durch \emph{vollständige} Resolution 

$(A_1\vee x,\ldots,A_p\vee x)$
mit 
$(\neg x\vee B_1,\ldots,\neg x \vee B_q)$

\bigskip

Übung: unit propagation als Spezialfall

Projekt: SAT-Solver bzw. Präprozessor bauen
\end{slide}
