Lösungsplan: SAT-Kodierung

Ansatz:

• jede elementare Formel (x = y mathend000#) durch eine boolesche Unbekannte (e_{x, y} mathend000#) ersetzen
• und Transitivität der Gleichheitsrelation kodieren

EQUALITY_CONSTRAINTS ist NP-vollständig, denn:

• E.C. ∈ mathend000# NP (laut Ansatz)
• SAT ≤_P mathend000# E.C. (Übung)

Verbesserungen (durch Analyse des Gleichheitsgraphen):

• Verkleinerung der Formeln (Entfernen von Variablen)
• Verringerung der Anzahl der Constraints für Transitivität