\begin{slide}{Gleichheitsgraph (equality graph)}

\begin{itemize} \itemsep 2pt
\item Knoten: Variablen
\item Kanten $xy$, falls $x=y$ oder $x\neq y$ in $M$ vorkommt 
  (Gleichheitskante, Ungleichheitskante)
\end{itemize}
(logische Verknüpfungen werden ignoriert!)

\emph{Widerspruchskreis:}
\begin{itemize}
\item geschlossene Kantenfolge
\item genau eine Ungleichheitskante
\item einfach (simple): kein Knoten doppelt
\end{itemize}

falls die Kanten eines solchen Kreise mit \emph{und} verknüpft sind,
dann ist die Formel nicht erfüllbar.

\end{slide}
