Gleichheitsgraph (equality graph)

• Knoten: Variablen
• Kanten xy, falls x = y oder x $\neq$ y in M vorkommt (Gleichheitskante, Ungleichheitskante)

(logische Verknüpfungen werden ignoriert!)

Widerspruchskreis:

• geschlossene Kantenfolge
• genau eine Ungleichheitskante
• einfach (simple): kein Knoten doppelt

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