Idee

Constraints für ganze Zahlen

• plus, minus, mal, min, max, ...
• boolesche Verknüpfungen

die Zahlen werden ,,gesprengt`` (blast = Explosion)

und man rechnet mit ihren Bits (CNF-SAT)

(nach Festlegung der Bitbreite der Zahlen)

x = [x₀, x₁,..., x_w-1]

Notation hier: LSB ist links