City Research Online

Abstract

“Bit-blasting”: reducing terms in the theory of bit-vectors to formulae in propositional logic, is a popular and effective technique. For logical operations, comparisons and even bit-vector addition, it produces circuits or CNF clauses that are linear in the size of the bit-vector formula and unit propagation gives effective bit-wise reasoning. However bit-blasting is highly limited when it comes to multiplication. The formulae produced are at least one order of magnitude larger than other terms and introduce significant difficulty into the SAT problem. Even basic awareness of modular (2ⁿ) arithmetic and the vast body of arithmetic, algebraic and cryptographic theorems on it, make it clear that bit-blasting is the wrong path for handling multiplication. In this work-in-progress paper we sketch two further steps along this wrong path, compacting multiplication by constants and showing the existence of incremental encodings of multiplication. It is hoped that these will not only get us closer to “the best that can be achieved given the limitations” but also that they might eventually connect to less limited, algebraic techniques.

Publication Type:	Conference or Workshop Item (Paper)
Additional Information:	Copyright © 2021Martin Brian. Published under the Creative Commons License Attribution 4.0 International (CC BY 4.0).
Subjects:	Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments:	School of Science & Technology School of Science & Technology > Department of Computer Science
SWORD Depositor:	Symplectic Administrator

Export

Downloads