\documentclass{slides}
\usepackage{amsmath,amssymb,latexsym}
\begin{document}

\slide

\begin{center}
Resolution und 2-SAT
\end{center}
Klausel: \\
Menge (= Disjunktion) von AL-Literalen\\[3mm]
AL-Formel in Klauselform: \\
Menge (= Konjunktion) von Klauseln 
$\simeq$ POSE\\[3mm]
$\Box$ = leere Klausel = leere Disjunktion = FALSE\\[3mm]
Resolution:\\
Generierung von neuen Klauseln aus vorhandenen Klauseln
mittels der Regel
\[
{\{x\} \cup \alpha ~~,~~ 
\{\overline{x}\}\cup \beta 
\over \alpha \cup \beta}
\]
Hierbei sind $\alpha$, $\beta$ beliebige (auch leere) Klauseln.\\[3mm]
Ist $F$ AL-Formel (in Klauselform) und $\alpha$ Klausel:
\[
F \vdash \alpha ~: ~
\begin{cases}
\text{$\alpha$ l\"asst sich aus $F$ in endlich vielen}\\
\text{Resolutionsschritten erzeugen}
\end{cases}
\]

\slide

Theorem:
\[
F~\text{unerf\"ullbar}~~\Longleftrightarrow~~
F \vdash \Box
\] 
Beweis der Korrektheit ($\Longleftarrow$):\\
Resolutionsschritte erhalten die
Erf\"ullbarkeit; die leere Klausel $\Box$ ist
aber unerf\"ullbar.\\[3mm]
Beweis der Ad\"aquatheit (Vollst\"andigkeit, $\Longrightarrow$):\\
$F = F(x_1,x_2,\ldots,x_n)$\\
$F_{x_1=0} =F(0,x_2,\ldots,x_n)$ geht aus $F$ hervor, indem man:\\
-- Klauseln, die $\overline{x_1}$ enthalten, eliminiert\\
-- in Klauseln, die $x_1$ enthalten, $x_1$ eliminiert\\
-- alle \"ubrigen Klauseln unver\"andert l\"asst\\[3mm]
$F_{x_1=1} = F(1,x_2,\ldots,x_n)$ wird analog definiert

Beachte:
\[
F \equiv (x_1 \vee F_{x_1=0} ) \wedge
(\overline{x_1} \vee F_{x_1=1})
\]

Insbesondere:
\[
F ~\text{erf\"ullbar}~~ \Longleftrightarrow~~
F_{x_1=0} \vee F_{x_1=1}~ \text{erf\"ullbar}
\]

\slide

Konsequenz:
\[
F~\text{unerf\"ullbar}~~\Longrightarrow~~
F_{x_1=0} ~\text{und}~ F_{x_1=1}~ \text{unerf\"ullbar}
\]

Induktion:
\[
F~\text{unerf\"ullbar}
~~\Longrightarrow~~
F_{x_1=0} \vdash \Box~~\text{und}~~F_{x_1=1} \vdash \Box
\]
Einsetzen von $x_1$ bzw, $\overline{x_1}$ in die Klauseln,
aus denen diese Literale vorher (bei Konstruktion von
$F_{x_1=0}$ bzw. $F_{x_1=1}$) entfernt wurden, liefert
\begin{align*}
\text{aus}~ F_{x_1=0} \vdash \Box :
~~~F \vdash \Box ~~&\text{oder}~~F
\vdash \{x_1\} \\ 
\text{aus}~ F_{x_1=1} \vdash \Box:
~~~F \vdash \Box ~~&\text{oder}~~F
\vdash
\{\overline{x_1}\}
\end{align*}
Zusammen also in jedem Fall
\[
F \vdash \Box
\]

\slide

$F = F(x_1,x_2,\ldots,x_n)$ Instanz von 2-SAT, d.h. AL-Formel in
Klauselform mit $\leq 2$  Literalen pro Klausel

$G_F = (V,E)$ : gerichteter Graph mit
\[
\text{Knoten}~V = \{0,1\} \cup
\{x_1,\overline{x_1},x_2,\overline{x_2}, \ldots,x_n,\overline{x_n}\}
\]
und den Kanten:
\begin{align*}
\text{f\"ur jedes Literal}~ \alpha~~: &~~~
\begin{cases}
~~\alpha \rightarrow 1 \\
~~0 \rightarrow \alpha
\end{cases} \\
\text{f\"ur jede $F$-Klausel } ~\{\alpha\}~~: &~~~
\begin{cases}
~~\overline{\alpha} \rightarrow 0 \\
~~1 \rightarrow \alpha
\end{cases} \\
\text{f\"ur jede $F$-Klausel } ~\{\alpha,\beta\}~~: &~~~
\begin{cases}
~~\overline{\alpha} \rightarrow \beta \\
~~\overline{\beta} \rightarrow \alpha
\end{cases} 
\end{align*}

\slide

Resolution
\[
\Big\{
\{\alpha,\beta\} , \{ \overline{\beta},\gamma\} \Big\}
\vdash \{ \alpha,\gamma \}
\]
bedeutet im Graphen  $G_F$ das Verketten von Kanten bzw. Wegen, 
d.h. f\"ur  alle $\alpha, \beta \in V$ (incl. 0 und 1) gilt
\[
F \vdash \{\alpha,\beta\}
~\Longleftrightarrow ~
\begin{cases}
\text{es gibt einen Weg in}~G_F\\
\text{von}~\overline{\alpha}~\text{nach}~\beta~(\text{
und somit }\\
\text{auch von}~\overline{\beta}~\text{nach}~Ê\alpha)
\end{cases}
\]

\slide

Folgende Aussagen sind \"aquivalent:
\begin{itemize}
\item
$F$ ist unerf\"ullbar 
\item
$F \vdash \Box$ 
\item
es ex. $\alpha \in V$ mit
$
F \vdash ~\{\alpha\}~\text{und}~
F \vdash \{\overline{\alpha}\}
$
\item
es gibt ein $\alpha \in V$ mit einem Weg von $\alpha$ nach
$\overline{\alpha}$ und einem Weg von $\overline{\alpha}$
nach $\alpha$ in $G_F$
\item
es gibt ein $\alpha \in V$ mit 
\[
\overline{\alpha} \rightarrow \ldots \rightarrow 0 \rightarrow \alpha
\rightarrow \ldots \rightarrow 0 \rightarrow \overline{\alpha}
\]
bzw.
\[
1  \rightarrow \ldots \rightarrow \alpha \rightarrow 1
\rightarrow \ldots \rightarrow \overline{\alpha}  \rightarrow 1
\]

\slide

\item
f\"ur alle $\alpha \in V$ gilt
\[
\overline{\alpha} \rightarrow \ldots \rightarrow 0 \rightarrow \alpha
\rightarrow \ldots \rightarrow 0 \rightarrow \overline{\alpha}
\]
bzw.
\[
1  \rightarrow \ldots \rightarrow \alpha \rightarrow 1
\rightarrow \ldots \rightarrow \overline{\alpha}  \rightarrow 1
\]
\item
$G_F$ ist stark zusammenh\"angend:  zu je  zwei Literalen
$\alpha,\beta \in V$ gibt es einen Weg von $\alpha$ nach $\beta$
\end{itemize}

Ordnungstheoretische Interpretation:

Die Relation $\leq _F$ mit
\[
\overline{\alpha} \leq_F \beta~~\Leftrightarrow~~
\overline{\beta} \leq_F \alpha ~~\Leftrightarrow~~
F \vdash \{\alpha,\beta\}
\]
ist eine Pr\"aordnung auf $V$. 

\slide

Die induzierte
\"Aquivalenzrelation $\equiv_F$
\[
\alpha \equiv_F \beta~~\Longleftrightarrow~
\alpha \leq_F \beta~~\text{und}~\beta  \leq_F \alpha
\]
fasst Literale zu Klassen 
\[
[\alpha]_F = \{ \beta\,;\,\beta \equiv_F \alpha \}
\]
zusammen, die in jeder
erf\"ullenden Bewertung von
$F$ den gleichen Wahrheitswert erhalten m\"ussen.
Diese \"Aquivalenzklassen sind die (starken) 
Zusammenhangskomponenten des
Graphen $G_F$.
\\
Insbesondere m\"ussen alle Literale in
$[1]_F$ ``wahr'' und alle Literale in $[0]_F$ ``falsch''  sein.

Es gilt
\[
F~ \text{unerf\"ullbar}~~ \Leftrightarrow ~~[0]_F = [1]_F
\]

\end{document}