“Bit-blasting” : reducing terms in the theory of bit-vectors to formulae in propositional logic, is a popular and efective 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 efective 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 dificulty 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. No matter how far down the wrong road you've gone, turn back. - Turkish Proverb “Bit-blasting” is a technique for reducing first-order terms and predicates in the theory of bitvectors1 to propositional logic. Every bit in each bit-vector term is represented by a propositional literal and clauses are added that link them. Often additional proposition variables, so called intermediate variables, are used to control the size and complexity of the encoding. This reduction allows first-order (or “word-level”) equations to be solved using a SAT solver (or “bit-level” reasoning). Thus the immense (and on-going) improvements in SAT reasoning can be leveraged. Bit-blasting is often regarded as characteristic of SMT as a whole. Even though it is just one component in some modern solvers, and there are solvers such as COLIBRI [1] and iSAT3 [2, 3] that support the theory of bit-vectors without bit-blasting. It is easy to explain, easy to visualise and works very well2 It is not uncommon to find people who mistakenly believe that all of SMT is a variant on this technique.
Section 2 discusses the current state-of-the-art and explains why multiplication (and other “non-linear” operations) remain and likely will always be, cumbersome and dificult to handle via bit-blasting. Having tried to convince the reader that this is the wrong path, Sections 3 and 4 outline our work-in-progress on improving the performance and reducing the overheads of bit-blasting multiplication. No performance data is given as we only have prototype implementations and a number of algorithmic questions remain open. There is also a question over what would be appropriate benchmarks. Although it is easy to come up with synthetic benchmarks (factoring, associativity, etc.) it is not clear how relevant they are. As there has been a co-evolution of solvers and benchmarks, there is a shortage of graduated and calibrated non-linear bit-vector problems.
Bit-blasting implementations tend to convert each term or predicate independently3. For each
operator there is a small section of program which produces the bit-blasting. We will refer to the
program and the output interchangeably as their encoding or the circuit. Some implementations
produce CNF directly, but it is more common to produce a propositional circuit form. These
may be And-Inverter Graphs (AIG) or they may allow other logical gates, with XOR being
particularly useful. Bit-level constant propagation and rewriting is applied to this, either
onthe-fly or after the whole expression has been converted. If circuits are produced an encoding,
such as Plaisted-Greenbaum [
The encodings used for each operator can be evaluated in terms of a number of metrics. The
easiest but least predictive of performance is the size: either the number of clauses or the number
of intermediate variables produced. More useful in the small scale is whether the encoding is
propagation complete (with respect to unit propagation) [
Table 1 shows the current best known encodings for each of the bit-vector operators of length
. Operations that move and duplicate bits in a fixed pattern are efectively free because they
can be encoded by simply renaming propositional literals. Likewise negation can be encoded
by changing the polarity of the literals input. Operations that are ‘bit-parallel’ can be encoded
with a circuit for each bit. So bvand needs one AND gate (3 clauses) per bit and bvxor needs
one XOR gate (4 clauses) per bit. The non-standard bit-vector if-then-else (bvite) is bit-parallel
but shows an interesting efect. The smallest encoding is not propagation complete. This
happens with more complex operations, including multiplication. Smaller encodings do not
3Experience from [
4Which, of course, is then pre-processed by the SAT solver. We will follow the conventions of the literature and ignore this important step.
5Whether assignments to intermediate variables are considered in propagation completeness is a subtle but significant point that is often ignored in the literature. Operators concat, extract, repeat rotate_left, rotate_right zero_extend, sign_extend bvnot bvand, bvor, bvnand, bvnor bvxor, bvxnor bvite bvcomp bvult, bvule, bvugt, bvuge, bvslt, bvsle, bvsgt, bvsge bvneg bvadd, bvsub bvshl, bvlshr, bvashr bvmul, bvudiv, bvurem, bvsdiv, bvsmod
CNF 0 0 0 0 3 4 4 / 6 4 + ( + 1) 6 7 14 ( log()) (2) ( log()) (2) ✓ ✓ × × necessarily propagate as well and encodings that propagate well are not necessarily small. Thus it is important to be clear about which metrics we are aiming to improve.
Most of the arithmetic operations make use of additional intermediate or auxiliary variables. For example in comparisions it is useful to have ‘the previous bits match’ propositions. Likewise addition can be built from full-adders and intermediate ‘carry’ propositions.
The first operations for which no propagation complete encodings are known are shifts. The author believes that they can be created, but will likely increase the size of the encoding by a constant factor. Note that shifts by a constant amount are a special case and are efectively zero cost, like other static bit shufling.
There are a very large number of possible encodings for multiplication. Without more useful metrics and ways of comparing them (a work-in-progress) it is hard to explore this space in a meaningful way. The most obvious (and popular) encoding is based on the shift-add algorithm: bv multiplier_encoding(bv lhs, bv rhs) { int n = lhs.length(); bv intermediate[n]; intermediate[0] = and(repeat(n,lhs[0]), rhs); for (int i = 1; i < n; ++i) { intermediate[i] = add(intermediate[i-1],
lshift(and(repeat(n,lhs[i]), rhs), i)); }
return intermediate[n-1]; Here bv are data types that store a vector of propositional variables, one for each bit of the bitvector. repeat, and, lshift and plus are functions that generate the appropriate encoding.
The intermediate variables need * propositional variables, plus * − 1 auxiliary variables from the additions. There are * 3 * clauses from the and operations and ( − 1) * 14 * clauses from the additions. If = 32 then this is 2, 016 variables and 16, 960 clauses. If = 64 then this is 8, 128 variables and 68, 736 clauses for a single multiplier!
Knuth [
Limits of Multiplier Encodings How much could this be improved? A number of results
suggest that there are likely to be fundamental limits. Schönhage and Strassen [
Reversing this argument, we can obtain a size bound on a propagation complete encoding of
multiplication. Given = * with and prime, a propagation complete encoding could be
used to factor in at most calls to unit-propagation by incrementally calling unit-propagation
and then fixing bits of if they are not set by the encoding. This would give a factoring algorithm
that would run in (2) steps where is the size of the set of clauses. As the best known
algorithms for this task are pseudo-polynomial, the existence of polynomial-sized propagation
complete multipliers seems unlikely. Our experience in [
So, having shown that improved encodings for multiplication6 are likely to still be large and will only propagate better when very large, we conclude that algebraic techniques (such as incremental computation of Groebner bases) are much more likely to be efective and suggest future researchers pursue those.
In the rest of the paper we will ignore this advice.
For most bit-vector operators, constant propagation and some minor rewriting ((bvand a a) → a) during bit-blasting is enough produce optimised encodings when one operand is constant. When using the shift-add multiplier above, normalising symmetry so that lhs is the constant will reduce the number of additions to the number of 1s in lhs minus one. For program analysis 6In the naïve encoding, divide and remainder are both even more expensive. However rewriting them using the defining identity / * + = reduces them to basically multiplication (if you ignore divide by zero...). (apart from cryptography) this is generally suficient as most constants are small. However for lfoating-point multiplication by constant, we need to consider more varied bit-vector constants.
Consider 127 * x. The shift-add multiplier with constant propagation would give: 127 * x = x«6 + x«5 + x«4 + x«3 + x«2 + x«1 + x However 127 is a diference between powers of 2, so we can compute it as:
127 * x = (128 - 1)*x = x«7 - x So we have dropped from 6 additions down to just one. By treating contiguous sections of 1s in this way we can reduce the number of additions to the number of parity changes in the number. This is a significant saving in the average case but the worst-case, 01010101..., is still no better than the shift-add approach above.
This inspires our next trick; if the constant contains repeated patterns then we can use sharing of expressions to reduce the number of additions. For example:
0x5555 * x = (0x55«16 + 0x55) * x = (0x55 * x) « 16 + (0x55 * x). Iterating this we can compute multiplication by 0x5555 using just 3 additions, rather than the 8 required previously. By combining these two techniques we can achieve an asymptotic (and significant) improvement over the shift-add encoding.
Unfortunately, it is not immediately obvious how to best combine these two; consider 0b10111011 * x. If we use shift-add multiplication with constant rewriting then this will require 5 additions. Using subtraction of powers of two to create regions of 1s we can compute it with 4 additions: 0b10111011 * x = x«7 + (0b111 * x)«3 + (0b11 *x)
= x«7 + (x«3 - x)«3 + (x«2 - x) However using the repeated pattern trick first requires just 3 additions, a 40% reduction from our starting encoding: 0b10111011 * x = (0b1011 * x) « 4 + (0b1011 * x)
0b1011 * x = x«3 + (x«2 - x)
Before developing an algorithm, it is worth considering the context. It is relatively rare for
lfoating-point multiplications by constants to be encountered on their own. Weighted sums,
vector and matrix multiplication and evaluating neural networks will often multiply the same
number by several diferent constants. It is possible and desirable to share the same sub-terms
between multiplications by diferent constants. Unfortunately [
A very common idiom in verification is “The full problem is very dificult or impossible, but how much of it do we actually need to do?”. One way this is realised is via approximations. If the full bit-blasting is large and adds complexity to the SAT solver, why not use an approximation and refine as needed? Bryant et al. [ 14] proposes this idea but practical implementations run into problems due to the lack of incremental encodings of multiplication. Using a variant of the Toom-Cook multiplication algorithm [15, 16], with non-determinism rather than Gaussian elimination, it is possilbe to create a series of encodings that over-approximate multiplication and allow for incremental tightening of the approximation.
Consider multiplying two 16-bit numbers7 c = a * b. We write each input as concatenations of 4-bit components, a = a3:a2:a1:a0 and b = b3:b2:b1:b0. Rather than computing the multiplication directly, let and be polynomials in such that (16) = a and (16) = b: () = () = a33 + a22 + a1 + a0 b33 + b22 + b1 + b0 we will refer to these as component polynomials. If we define to be the product of the component polynomials: () = () * () =
d66 + d55 + d44 + d33 + d22 + d1 + d0 then:
a * b = (16) * (16) = (16) = c By computing the coeficients of we can evaluate the polynomial and obtain c: c =
d6«24 + d5«20 + d4«16 + d3«12 + d2«8 + d1«4 + d0 We could compute the coeficients of directly but if we allow them to be non-deterministic, we can constrain the value of on any 7 points and by polynomial interpolation, the coeficients will have the unique, correct value. Critically, we can add these 7 constraints incrementally during the solving process, with each reducing the degree of over-approximation. By picking our evaluation points to be small positive and negative powers of two, the size of the multiplications we perform are greatly reduced: (0) = (0) * (0)
= a0 * b0 (1) = (1) * (1) (− 1) = (− 1) * (− 1)
= ((a2 + a0) + (a3 + a1)) * ((b2 + b0) + (b3 + b1)) 7For simplicity of explanation we will omit the extensions and computation of necessary bit-widths. This turns out to be a significantly more fiddly process than might be expected =
((a2 + a0) − (a3 + a1)) * ((b2 + b0) − (b3 + b1)) (2) (− 2) = (2) * (2) = ((a2«2 + a0) + (a3«1 + a1)«1) * ((b2«2 + b0) + (b3«1 + b1)«1) = (− 2) * (− 2) = ((a2«2 + a0) − (a3«1 + a1)«1) * ((b2«2 + b0) − (b3«1 + b1)«1) ...
This produces correct results but computing 7 (= 2 * (/) − 1) small multiplications instead of one large multiplications is not necessarily a saving. Extensive experimentation 8 suggests that it is a net reduction in clauses and variables for 64-bit multipliers and the 24/48 and 53/106 bit multipliers needed for float32 and float64. But this is dependant on which evaluation points are used, the number of components, etc.
However, there remain a number of open questions about this approach:
• What is the best strategy for picking the component size? Longer components mean less
constraints but make the multiplications in them larger. Small components mean more
constraints and can reduce the size of the multiplication but evaluation at larger powers
of 2 will negate this. Optimising for cases where we can use existing small propagation
complete multipliers [
By blindly ignoring the right, algebraic path and continuing to try to step-wise improve the bit-blasting of multiplication we have found ourselves with a number of algebraic questions about the behaviour of polynomials over modulo 2 arithmetic. The author considers this an entertainingly ironic place to finish a paper.
8Many thanks to Kevin Stefanov for his work on these.
The author would like to thank Kevin Stefanov for his work on a prototype of the Toom-Cook multiplier and Florian Schanda and the anonymous referees of SMT21 for their myriad of suggestions. [14] R. Bryant, D. Kroening, J. Ouaknine, S. Seshia, O. Strichman, B. Brady, Deciding Bit-Vector Arithmetic with Abstraction, volume 4424 of Lecture Notes in Computer Science, SpringerVerlag, Heidelberg, Germany, 2007, pp. 358–372. doi:10.1007/978-3-540-71209-1_ 28. [15] A. L. Toom, The Complexity of a Scheme of Functional Elements Realizing the Multiplication of Integers, Soviet Mathematics - Doklady (1963) 714–716. [16] S. A. Cook, On the Minimum Computation Time of Functions, Ph.D. thesis, Harvard University, 1966.