SMT solving
Bit-blasting
Translating fixed-width operations into Boolean constraints on individual bits.
Definition
Bit-blasting
Bit-blasting lowers a bit-vector formula into a Boolean circuit or CNF formula.
The resulting SAT problem represents each output bit of operations such as addition and multiplication. Correctness depends on the translation preserving the original bit-vector semantics.
01
Example
A two-bit adder becomes Boolean constraints for two sum bits and a carry bit.
02
Important distinction
A SAT certificate checks the lowered Boolean problem, so the bit-blasting translation remains a separate trust boundary unless it is also checked.
After reading this article, you should be able to
- Define Bit-blasting in the sense used on this site.
- Describe the information preserved when a bit-vector term is lowered to SAT.