\begin{slide}{Vorverarbeitung}

Niklas Eén, Armin Biere: 
\emph{Effective Preprocessing in SAT Through Variable and Clause Elimination.}
 SAT 2005: 61-75
\url{http://dx.doi.org/10.1007/11499107_5}
\url{http://minisat.se/downloads/SatELite.pdf}

\begin{itemize}\itemsep 0pt \parskip 1pt
\item clause distribution:

  Elimination einer Variablen $y$
  durch vollständige Resolution 
  (Fourier-Motzkin-Verfahren):
  
  jede Klausel $C\ni y$ resolvieren gegen
  jede Klausel $C' \ni \overline{y}$,

  Originale löschen
\item self-subsumption resolution (evtl. Übung)
\end{itemize}

Implementierung
muß Subsumption von 
Klauseln sehr schnell feststellen
(wenn $C_1\subseteq C_2$, kann $C_2$ entfernt werden)

\end{slide}
