Reduktion zu Aussagenlogik (I)

• Plan: jede elementater Formel (x = y mathend000#) durch eine boolesche Variable ersetzen, dann SAT-Solver anwenden.
• Widerspruchskreise sind auszuschließen: in jedem Kreis darf nicht genau eine Kante falsch sein.

  dadurch wird die Transitivität der Gleichheitsrelation ausgedrückt.

• es gibt aber exponentiell viele Kreise.