\begin{slide}{Kleine Welt}

für Gleichheits-Constraints mit $n$ Variablen $x_1,\ldots, x_n$:

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

das kann man reduzieren:

Wenn ein solches Gleichheits-System erfüllbar ist,
dann besitzt es auch ein Modell mit $\le n$ Elementen.

(Beweis-Idee: schlimmstenfalls sind alle Variablenwerte verschieden)

Den Wert jeder Variablen kann man also mit $\log n$ Bits kodieren.

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

\end{slide}
