\begin{slide}{Resolution}


  \begin{itemize}
  \item 
ein Resolutions-Schritt:
\[ 
\frac{(x_1 \vee \ldots \vee x_m \vee y), (\neg y \vee z_1 \vee \ldots \vee  z_n)}
{x_1 \vee \ldots \vee x_m \vee z_1 \vee \ldots \vee  z_n}
\]
\item Sprechweise: 
Klauseln $C_1,C_2$ werden nach $y$ \emph{resolviert}.
\item
Schreibweise: $C = C_1 \oplus_y C_2$
\item Beispiel: 
\[
\frac{x\vee y,y\vee \neg z}{x\vee\neg z}
\]
\item
Satz: $\{C_1,C_2\} \models C_1\oplus_y C_2$. (Die Resolvente folgt aus den Prämissen.)
  \end{itemize}

\end{slide}
\begin{slide}{Resolution als Inferenzsystem}

mehrere Schritte:
\begin{itemize}\itemsep 2pt \parskip 2pt
\item Schreibweise: $M\vdash C$
\item Klausel $C$ \emph{ist ableitbar} aus Klauselmenge $M$
\item Definition: 
  \begin{itemize}
  \item (Induktionsanfang) wenn $C\in M$, dann $M\vdash C$ 
  \item (Induktionsschrit)

    wenn $M\vdash C_1$ und $M\vdash C_2$, dann $M\vdash C_1\oplus_y C_2$
  \end{itemize}
\end{itemize}
Beachte Unterschiede:
\begin{itemize}\itemsep 2pt \parskip 2pt
\item Ableitung $M\vdash C$ ist \emph{syntaktisch} definiert (Term-Umformung)
\item Folgerung $M\models C$ ist \emph{semantisch} definiert (Term-Auswertung)
\end{itemize}


\end{slide}

\begin{slide}{Resolution und Unerfüllbarkeit}

Satz: $\Mod(F)=\emptyset \iff F\vdash \emptyset$
\quad
(in Worten: $F$ in CNF nicht erfüllbar $\iff$
aus $F$ kann man die leere Klausel ableiten.)

\begin{itemize}\itemsep 0pt \parskip 0pt
\item  Korrektheit ($\Leftarrow$): Übung.
\item Vollständigkeit ($\Rightarrow$): 
Induktion nach $|\Var(F)|$
\end{itemize}

dabei Induktionsschritt: 
\begin{itemize}\itemsep 0pt \parskip 0pt
\item 
betrachte $F$ mit Variablen
$\{x_1,\ldots,x_{n+1}\}$.
\item
Konstruiere $F_0$ (bzw. $F_1$) aus $F$ \\
durch \glqq Belegen von $x_{n+1}$
mit 0 (bzw. 1) \grqq  

(d. h. Streichen von Literalen und Klauseln)
\item
Zeige, daß $F_0$ und $F_1$ unerfüllbar sind.
\item wende Induktionsannahme an: $F_0\vdash\emptyset,F_1\vdash \emptyset$
\item kombiniere diese Ableitungen
\end{itemize}

\end{slide}

\begin{slide}{Resolution, Bemerkungen}

\begin{itemize}\itemsep 1pt
\item Unit Propagation kann man als Resolution auffassen
\item moderne SAT-Solver 
  können Resolutions-Beweise 
  für Unerfüllbarkeit ausgeben
\item es gibt nicht erfüllbare $F$ mit (exponentiell) 
  großen Resolutionsbeweisen
  (sonst wäre NP $=$ co-NP, das glaubt niemand)
\item komprimiertes Format für solche Beweise 
  (RUP---reverse unit propagation)
  wird bei ``certified unsat track'' der 
  SAT-competitions verwendet  (evtl. Übung)  
\item vollständige Resolution einer Variablen $y$
  als Preprocessing-Schritt
\end{itemize}

\end{slide}
