\begin{slide}{Idee}

Constraints für ganze Zahlen
\begin{itemize}
\item plus, minus, mal, min, max, \dots
\item boolesche Verknüpfungen
\end{itemize}
die Zahlen werden \glqq gesprengt\grqq\ (blast $=$ Explosion)

und man rechnet mit ihren Bits (CNF-SAT)

(nach Festlegung der Bitbreite der Zahlen)

\bigskip

$x = [x_0,x_1,\ldots,x_{w-1}]$

Notation hier: LSB ist links
\end{slide}

