
\begin{slide}{Reduktion zu Aussagenlogik (I)}

  \begin{itemize}
  \item Plan: jede elementater Formel ($x=y$)
    durch eine boolesche Variable ersetzen,
    dann SAT-Solver anwenden.
  \item Widerspruchskreise sind auszuschließen:
    in jedem Kreis darf nicht genau eine Kante falsch sein.

dadurch wird die Transitivität der Gleichheitsrelation ausgedrückt.
  \item es gibt aber exponentiell viele Kreise.
  \end{itemize}


\end{slide}

\begin{slide}{Reduktion zu Aussagenlogik (II)}

\emph{Satz} (Bryant und Velev, CAV-12, LNCS 1855, 2000):

es genügt, Transitivitäts-Constraints
für sehnenlose Kreise hinzuzufügen.

\bigskip

\emph{Satz} (Graphentheorie/Folklore):

zu jedem Graphen $G$ kann man in Polynomialzeit
einen chordalen Obergraphen $G'$ konstruieren
(durch Hinzufügen von Kanten).

\bigskip

Graph $G$ heißt \emph{chordal},
wenn er keinen sehnenlosen Kreis einer Länge $\ge 4$ enthält.

\bigskip

\emph{Vorsicht}: chordal $\neq$ trianguliert, Beispiel.

\bigskip

\emph{Algorithmus}: wiederholt: einen Knoten entfernen,\\
dessen Nachbarn zu Clique vervollständigen.


\end{slide}
