Idee

Constraints für ganze Zahlen

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

und man rechnet mit ihren Bits (CNF-SAT)

(nach Festlegung der Bitbreite der Zahlen)


x = [x0, x1,…, xw-1] mathend000#

Notation hier: LSB ist links



2014-03-31