Bitblasting

Lösen von Constraint-System über ganzen Zahlen:

• Festlegen einer maximalen Bitbreite
• unbekannte Zahl ⇒ Folge von unbekannten Bits
• arithmetische Operationen ⇒ Bit-Operationen (entspr. Schaltkreis-Entwurf)
• Lösung durch SAT-Solver

Beispiel: http://dfa.imn.htwk-leipzig.de/satchmo/