Gleichheitsgraph (equality graph)

• Knoten: Variablen
• Kanten xy mathend000#, falls x = y mathend000# oder x≠y mathend000# in M mathend000# 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.