\begin{slide}{Lösungsplan: SAT-Kodierung}

Ansatz:
\begin{itemize} \itemsep 0pt
\item jede elementare Formel ($x=y$) durch
  eine boolesche Unbekannte ($e_{x,y}$) ersetzen
\item und Transitivität der Gleichheitsrelation kodieren
\end{itemize}

EQUALITY\_CONSTRAINTS ist NP-vollständig, denn:
\begin{itemize}\itemsep 0pt
\item E.C. $\in$ NP (laut Ansatz)
\item SAT $\le_P$ E.C.  (Übung)
\end{itemize}

Verbesserungen (durch Analyse des \emph{Gleichheitsgraphen}):
\begin{itemize}\itemsep 0pt
\item Verkleinerung der Formeln (Entfernen von Variablen)
\item Verringerung der Anzahl der Constraints
  für Transitivität
\end{itemize}


\end{slide}
