Fast Three-Valued Abstract Bit-Vector Arithmetic
summary
The work gives polynomial-time algorithms that compute the best three-valued abstract result for bit-vector addition and multiplication: addition in linear time and multiplication in worst-case quadratic time. It reforms arithmetic as pseudo-Boolean modular inequalities via an hk modular reformulation (each output bit treated modulo 2^{k+1}), finds extremes to decide 0/1/x, and handles multiplication by sign flips plus a special-case for double-unknown column pairs. Implementation verifies equivalence with naive enumeration for n≤9, benchmarks show very fast addition and practical 32-bit multiplication, and code is available under CC0.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 5:15Forward operation problem (simplified definitions)
- 8:08Obtaining fast algorithms: pseudo-Boolean reinterpretation
- 10:27Modular extreme-finding technique
- 13:49Fast abstract addition: example 1/2
- 17:20Fast abstract multiplication: finding extremes
- 21:32Experimental evaluation: dependence on the number of unknown bits
- 22:26Conclusion