Kleine Welt

für Gleichheits-Constraints mit n mathend000# Variablen x₁,…, x_n mathend000#:

die hier gezeigte Kodierung benutzt n² mathend000# boolesche Variablen b_{i, j}$\iff$(x_i = x_j) mathend000#

das kann man reduzieren:

Wenn ein solches Gleichheits-System erfüllbar ist, dann besitzt es auch ein Modell mit ≤n mathend000# Elementen.

(Beweis-Idee: schlimmstenfalls sind alle Variablenwerte verschieden)

Den Wert jeder Variablen kann man also mit log n mathend000# Bits kodieren.

Erweiterung: man kann für jede Variable einen passenden (evtl. kleineren) Bereich bestimmen.