Idee

Constraints für ganze Zahlen

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

die Zahlen werden „gesprengt`` (blast = mathend000# Explosion)

und man rechnet mit ihren Bits (CNF-SAT)

(nach Festlegung der Bitbreite der Zahlen)

x = [x₀, x₁,…, x_w-1] mathend000#

Notation hier: LSB ist links