\begin{slide}{CNF-Kompression (Motivation)}
vereinfachte Annahme: SAT-Solver ist schneller, wenn
\begin{itemize}\itemsep 0pt
\item weniger (Zusatz-)Variablen
\item weniger Klauseln
\end{itemize}

führt zu der Aufgabe:
\begin{itemize}\itemsep 0pt
\item Eingabe: boolesche Formel $F$
\item Ausgabe: kleine zu $F$ (erfüllbarkeits)äquivalente CNF.
\end{itemize}

Anwendungen:
\begin{itemize}\itemsep 0pt
\item $F$ ist Halbadder, Volladder
\item $F$ ist Addition, Multiplikation usw. für geringe Bitbreite
\end{itemize}

Aber: mehr Klauseln $\Rightarrow$ mehr Propagationen

\end{slide}

\begin{slide}{CNF-Kompression (Implementierung)}

zu gegebener Formel $F$ bestimme Menge der \emph{Prim-Implikanten} 
$P=\{P_1,\ldots\}$, 

das sind \emph{minimale} Klauseln $P_i$ mit
$F\rightarrow P_i$

(minimal bezüglich Inklusion von Literalen)

\bigskip

dann bestimme eine kleinste Teilmenge $M \subseteq P$
mit $\bigwedge M \rightarrow F$.

das ist eine ganzzahlige lineare Optimierungsaufgabe
(Übung: welche?),
kann durch entsprechende Constraint-Solver gelöst werden
(glpsol, scip, clp)

\begin{small}
Diskussion: \url{http://groups.google.com/group/minisat/msg/012bb4712c7e90a7}

Anwendung: \url{https://github.com/jwaldmann/satchmo/blob/master/Satchmo/Binary/Op/Common.hs#L118}
\end{small}

\end{slide}
