Polynomials over bit-vectors, binary polynomials, are considered algebraically and it is observed that binary polynomials can be considered as a tree of subpolynomials. A construction of such subpolynomials is given. The application of these subpolynomials, along with other recent results on binary polynomials, in encoding polynomials over bit-vectors as part of solving SMT problems is investigated. Preliminary results are given. PCWrEooUrckResehdoinpgs ISSNc1e6u1r-3w-0s0.o7r3g
Evaluation of polynomials is a fundamental computational process. Polynomials are evaluated over some numerical or algebraic structure, be that fields or integer rings. Numbers need to be represented on a machine and this representation is usually in terms of bit-vectors. Polynomials over bit-vectors are referred to as binary polynomials. This paper is concerned with the evaluation of binary polynomials, with a particular interest in how this can be exploited as a component of solving SMT problems.
First-order terms and predicates in the theory of bit-vectors are typically handled in SMT solvers through bit-blasting, reducing numbers represented as bit-vectors to their constituent bits and reasoning propositionally about these. This means that reasoning about bit-vectors can take advantage of powerful SAT solving techniques. However, it is not clear that this is the right way to handle expressions involving multiplication since this can lead to some rather large representations (and/or representations that do not perform well). A short survey of the state-of-the-art, along with some suggestions as to improvements and a critique of the whole approach, can be found in [1].
Evaluating a polynomial potentially involves a lot of multiplication, so there is some hope that investigating alternative ways of handling polynomials might lead to a big pay-of in terms of the performance of SMT problems over bit-vectors. This might be particularly important since non-linear problems represent a hard challenge within formal verification, with SMT solvers being the main engine for doing this.
The theory of bit-vectors contains several sub-algebras. If bit-vectors are interpreted as unsigned binary numbers then there is a ring isomorphism with integers modulo 2 (where is the bit-width). This means that binary polynomials also form a ring. The challenge is to leverage the algebraic structure of binary polynomials to better manipulate inputs so that when they are eventually bit-blasted evaluation within SMT solvers is improved.
Noting that bit-vectors modulo 2 are equivalent to finite rings, two main results are observed and exploited in this work. Firstly, the observations made in [2] are reiterated, in particular that binary polynomials can be expressed in a normal form with a maximum degree dependent on the bit-width. Secondly, a new technique is introduced noting the finite nature of binary polynomials means that a polynomial can be broken down into smaller subpolynomials; the construction and algorithms for doing so are presented.
The complexity of polynomials pulls in several directions. Firstly, there is the degree of the polynomial being considered, which initially appears to be potentially unbounded. Secondly, there is the number of variables that the polynomial is over. Thirdly, there is the number and complexity of the monomials that are summed to give the polynomials (clearly this is partly dependent on the number of variables that the polynomial is over). Fourthly, there is the bit-width of the bit-vectors. This work restricts itself to univariate polynomials (that is, polynomials over one variable), hence monomials are simply powers of the variable; some pointers to results for multivariate polynomials will be given. Results concerning the degree of the polynomials considered are given in Section 2. Ultimately, interest is in typical machine representations of unsigned integers (8, 16, 32, 64 and 128 bits) and floating-point (24/48 and 53/106 bits), though worked examples will illustrate the arguments over smaller bit-widths.
The first part revisits the results from [ 2] and contextualises with other related literature. The second part investigates how polynomials change when their bit-width is reduced. The third part considers how the observations made in the first and second parts can be exploited in the encoding of polynomials for bit-blasting in SMT.
This paper makes the following contributions: • Introduces subpolynomials and investigates how they may be used to evaluate polynomials. • Applies recent results from [2] to reduce binary polynomials to a normal form with a maximum degree. • Performs an initial empirical investigation into the application of the above when solving SMT problems involving polynomials over bit-vectors.
The rest of the paper is structured as follows. Section 2 gives background and notation as well as surveying some of the related literature, in particular recent work on finding the maximum order for binary polynomials, given the bit-width. Section 3 gives results on polynomials for varying bit-width, Section 4 investigates how this can be exploited for evaluating polynomials over bit-vectors, Section 5 gives initial empirical results on this and Section 6 concludes.
This section formalises notation, whilst also surveying related work in the area. In particular, firstly results from [2] are summarised and illustrated, and secondly an overview of the evaluation of polynomials in general and in the context of SMT is provided.
A bit-vector with bit-width consists of a vector of 0/1 values denoted = [− 1, − 2, ..., 2, 1, 0]. This can be interpreted as an unsigned integer = 2− 1− 1 + 2− 2− 2 + ... + 222 + 21 + 0. These are treated as integers modulo 2, that is, − = 2 − . Being integer rings, there is no division operation, however, in some places something akin to division will be required in the form of a (zero-fill or logical) bit shift to the right, shR() = [0, − 1, − 2, ..., 2, 1].
A monomial is a product of variables, possibly raised to some power, and a coeficient. Powers are natural numbers and coeficients are integers. A polynomial is then a sum of monomials. This work considers only univariate polynomials (that is, with only one variable, hence monomials are a power of that variable multiplied by a coeficient). Hence polynomials have the form:
0 + 1 + 22 + ... + where ∈ N and ∈ Z (in much of this work coeficients will be reduced modulo 2). Such a polynomial is said to have degree , the maximum exponent of .
Considering integers modulo 2, knowing how an integer can be factored by 2 is important, since any integer that can be factored by 2 evaluates to 0, and any integer that can be factored by 2 and is then multiplied by 2 where + ≥ likewise evaluates to 0. This is formalised in the definition below. Definition 1. The 2-adic valuation of an integer, is a function 2 : Z → N ∪ {∞}, such that for integer , 2() is the largest such that ≡ 0 (mod 2), with 2(0) = ∞. This then satisfies: 1. 2() = 2() + 2(), 2. 2( + ) ≥ min( 2(), 2()).
For example, 2(
Definition 2. For ∈ N, let denote the smallest positive integer such that 2(!) ≥ .
For example, if = 2 for some ≥ 1, = + 2, if = 23, then = 10. 2.1.1. Canonical and factorial bases The usual representation of polynomials as a sum of monomials which are powers of , as above, is referred to here as the canonical basis for polynomials. Polynomials do not have to be represented in this way.
Let:
(0) = 1
(
These terms are referred to as factorial monomials, and a polynomial can then be represented as a sum of these factorial monomials. This alternative representation is referred to as the factorial basis. The degree of a polynomial in the factorial basis is the degree of the factorial monomial with the greatest and will denoted (). It will be seen below that this is an attractive representation of polynomials.
One of the dimensions of complexity discussed in the introduction was the degree of the polynomial. In [2] it was shown that for a given bit-width , any polynomial can be represented with a maximum degree − 1. Further, a polynomial given in the factorial basis is equivalent to one truncated to degree ( − 1). Moreover, a polynomial given in the canonical basis can be converted to a representation in the factorial basis, truncated, then converted back, giving a canonical basis representation of maximum degree − 1 in a normal form. These results are repeated and illustrated below along with an outline as to why they hold.
Key to the argument is the factorial basis. A factorial monomial represents a product in the form ( − 1)( − 2)...( − + 1), and when evaluated this becomes the product of a sequence of consecutive numbers. The product of consecutive numbers is divisible by !. If ≥ , then this product of consecutive numbers can be factored by 2, by the definition of , hence evaluates to 0 modulo 2. That is, the result of evaluating (), with ≥ , evaluates to 0. Hence any binary polynomial in factorial form whose degree is greater than or equal to is equivalent to another whose degree is at most − 1, indeed, in factorial form this is simply the truncation of higher degree terms. Since any polynomial over the factorial basis can be multiplied out to give a polynomial over the canonical basis, this maximum degree must also apply to binary polynomials over the canonical basis.
Given the bit-width it is possible to construct change of basis matrices that convert binary polynomials from the factorial basis to the canonical basis and vice versa. Taking the round journey of changing the basis from canonical to factorial and back again means that equivalent polynomials will be mapped to the same polynomial giving a normal form for binary polynomials.
To illustrate this, consider evaluating 3 + 3 + 22 + 43 + 24 + 36 + 27 for 4 bit numbers (that is, = 4 and = 6). The change of basis matrices for factorial to canonical (essentially multiplying out the factorial expression and reducing the coeficients mod 2) and canonical to factorial (the inverse of the first matrix) for degree 7 polynomials over bits are given below. ⎛ 1 0 0 0 0 0 0 0 ⎞ ⎜ 0 1 15 2 10 8 8 0 ⎟ ⎜⎜ 0 0 1 13 11 14 2 12 ⎟⎟ ⎜⎜ 0 0 0 1 10 3 15 8 ⎟⎟ ⎜⎜ 0 0 0 0 1 6 5 1 ⎟⎟ ⎜⎜ 0 0 0 0 0 1 1 15 ⎟⎟ ⎜⎝ 0 0 0 0 0 0 1 11 ⎠⎟ 0 0 0 0 0 0 0 1 ⎛ 1 0 0 0 0 0 0 0 ⎞ ⎜ 0 1 1 1 1 1 1 1 ⎟ ⎜⎜ 0 0 1 3 7 15 15 15 ⎟⎟ ⎜⎜ 0 0 0 1 6 9 10 13 ⎟⎟ ⎜⎜ 0 0 0 0 1 10 1 14 ⎟⎟ ⎜⎜ 0 0 0 0 0 1 15 12 ⎟⎟ ⎜⎝ 0 0 0 0 0 0 1 5 ⎠⎟ 0 0 0 0 0 0 0 1
Applying the second matrix to the input coeficient vector (
Polynomials are usually evaluated using Horner’s rule [3, 4, 5] (Knuth notes that a similar method can be found in earlier work of Isaac Newton and of Qin Jiushao [6]). With multiplication being more expensive than addition, reducing the number of multiplications used in evaluating a polynomial pays of even at the cost of extra additions. The rule provides a straightforward rearrangement of a polynomial so that evaluation requires multiplications and additions.
0 + 1 + 22 + ... + = 0 + (1 + (2 + ... + )...)
3 + 3 + 22 + 43 = 3 + (3 + (2 + 4))
Estrin’s method [7, 5] recursively decomposes a polynomial and might be attractive for higher-order polynomials when some parallelism is available. When it is known that a polynomial is going to be repeatedly evaluated (for example, as part of an approximation of a basic trigonometric function) then further up front manipulation can give better performance, for example for integers modulo polynomials of suficiently large degree can be evaluated with ( 2 + ()) multiplications [8, 6].
Bit-blasting, reducing a first-order SMT formula to a propositional SAT formula, remains a popular technique for handling the theory of bit-vectors. Each operator is encoded to its own circuit, either directly represented in CNF or using an intermediate form like And-Inverter Graphs (AIG) [9]. Then bitlevel constant propagation and rewriting will be applied before the formula is passed to the SAT solver. In addition to the propositional variables used to represent each first-order variable, intermediate variables are used extensively to reduce the number of clauses generated.
Many bit-vector operators bit-blast well. Operations that duplicate or move bits in a fixed patterns produce no propositional formula as they can be encoded using renaming. Other operations scale with the size of the bit-vectors, for example where is the bit-width, bvand requires 3 clauses per bit and no auxiliary variables, whilst a bvadd requires 14 clauses and auxiliary variables. Multiplication behaves less well, with encodings of multiplication being (2). This is the major cost in polynomial evaluation and is a major concern.
Whilst there are numerous ways to encode multiplication, the straightforward approach is often used, implementing the shift-add algorithm: bv multiplier_encoding(bv lhs, bv rhs) { int w = lhs.length(); bv intermediate[w]; intermediate[0] = and(repeat(w, lhs[0]), rhs); for (int i = 1; i < w; ++i) { intermediate[i] = add(intermediate[i-1],
lshift(and(repeat(w,lhs[i], rhs), i)); } } return intermediate[w-1];
The intermediate variables require × propositional variables, with × ( − 1) auxiliaries from additions. Then there are × 3 clauses from bit-vector and, as well as ( − 1) × 14 clauses from additions. If = 32 then a multiplier under this quadratic scheme has 2016 variables and 16960 clauses. Reduction steps, such as using Wallace trees [10] (as done by Bitwuzla [9]), can reduce the number of full adders used. The long-standing Schönhage-Strassen conjecture [11] states that the lower bound for multiplication of bit numbers is log(). This lower bound was reached in [12], however it is unclear whether this algorithm can be applied to bit-blasting in a way that is helpful.
Another property that is important for encodings is that they are propagation complete, that is, that all literals that are logically entailed can be inferred by unit propagation [13, 14]. Unfortunately the straightforward encoding of multiplication is not propagation complete and given that such an encoding could also be used for factoring it is unlikely that a polynomially sized propagation complete encoding of multiplication exists. 3. Polynomials modulo 2 This section makes some observations on polynomials over bit-vectors, noting that these are finite structures and can be decomposed in a tree-like way. Its main result is the construction of the polynomial over the high bits when the low bit is fixed. This will be exploited in the following section.
First consider an example, the polynomial () = 3 + 3 + 22 + 43 evaluated over four bit inputs, that is, modulo 24. This function is enumerated below ( = [3, 2, 1, 0]):
Now suppose that instead of four bits [3, 2, 1, 0] the polynomial is to be evaluated over three bits, [2, 1, 0]. It is easy to see that the output of () is just the restriction of the output above to the low three bits (repeated twice). This can be seen below tabulated as a).
What happens when instead of losing the top bit, the low bit is lost? The functions tabulated as b) and c) above give two slices of (), in b) where the low input bit is 0, and in c) where the low bit is 1. These functions can be described as polynomials over 3 bits. That in b) is 1 + 3 + 42, and that in c) is 6 + 3 + 42. In general, is there a polynomial to describe the functions described by these slices, and if so what are they?
The slices above are referred to as subpolynomials. Binary polynomials that describe these can be constructed as demonstrated in the proposition below. The proposition shows how a binary polynomial over bits leads to binary subpolynomials over the higher − 1 bits. In the statement, the treatment has used a right-shift to describe the constant term. The subpolynomial of resulting from fixing low bits [ , ..., 0] is a binary polynomial over − ( + 1) bits and will be denoted ...0 , for example, 0, 110, 011.
Proposition 1. Suppose = [− 1, ..., 1, 0] is a bit-vector of bit-width and that () = 0 + 1 + ... + is a univariate polynomial over these bits. For fixed low bit 0 the subpolynomial over the − 1 higher bits is denoted 0 . It is defined by slicing () on 0 and is given by: 0 () = shR( (0)) + ∑︁ ( )
=1 where each monomial maps as follows: In addition, the bit which is dropped by shR( (0)) is the output low bit of ().
Proof. The input to the function is = [− 1, ..., 1, 0] (that is, the low bit is fixed). Consider = [− 1, ..., 1], then = 0 +2. Consider () = (0 +2) = 0 +1(0 +2)+...+(0 +2). Expanding out each of the terms gives:
Noting that the coeficients for terms involving can always be factored by 2, the output low bit must be the low bit of the sum of the constant terms, that is, the remainder from the bit-shift. Bit-shifting the coeficients then gives the output for the higher bits, and renaming to variable leaves the results as given in the proposition.
Notice in the proof of the proposition that if the input low bit is 0 then only the diagonal gives a non-zero output. Also note that since the subpolynomial is over − 1 bits, the coeficients can be reduced modulo 2− 1.
Applying this to the example polynomial () = 3 + 3 + 22 + 43 when the input low bit is 0, the output 0() is below.
3 + 3 + 22 + 43 ↦→
=
=
shR(
It should be noted that the normalisation described in Section 2.2 has not been applied to the initial polynomial in this example.
Permutation polynomials over finite fields have been studied for a long time.
Definition 3. [15] A permutation polynomial is a polynomial over a finite field ≥ 1 if and only the polynomials permutes the elements of .
of order = ,
The standard definition is over finite fields and characterisation of what makes a polynomial a permutation polynomial has proved tricky. In contrast, [16] demonstrated that for binary polynomials (that is, where instead of finite field , there is a finite ring of order 2) there is an elegant characterisation for when the polynomial is a permutation polynomial.
Proposition 2. [16] A polynomial is a permutation polynomial mod 2 if and only if it has form 0 + 1 + 22 + 33 + ... where 1 (mod 2) = 1, 2 + 4 + ... (mod 2) = 0 and 3 + 5 + ... (mod 2) = 0.
Observe that whilst most polynomials over bit-vectors are not permutation polynomials, an arbitrary polynomial is the sum of a permutation polynomial and a small, highly structured, polynomial. Lemma 1. Given binary polynomial () = 0 + 1 + 22 + 33 + 44 + ... over 2, then () = () + () where () is a permutation polynomial and () = + 2 + 3, where , , ∈ {0, 1}.
Proof. Consider the three conditions characterising a permutation polynomial from Proposition 2. Firstly, if 1 (mod 2) = 1, then = 0, else = 1. Secondly, if 2 + 4 + ... (mod 2) = 0, then = 0, else = 1. Thirdly, if 3 + 5 + ... (mod 2) = 0, then = 0, else = 1. Observe that following these rules ensures that () = () + (), with () the permutation polynomial () = 0 + (1 − ) + (2 − )2 + (3 − )3 + 44 + ...
The first step when evaluating a binary polynomial is to consider whether its degree can be reduced as in Section 2.2 and [2] and if so, reduce it. The rest of this section firstly details evaluating a binary polynomial for an input, and secondly covers how this might then be utilised within bit-blasting.
The method for deriving subpolynomials given in the previous section then suggests an approach to evaluating binary polynomials. For a given input = [− 1, ..., 1, 0], for values of from 0 to − 1 calculate the output ℎ bit and derive the appropriate subpolynomial. Since the terms of the subpolynomials have constants that are rapidly rising powers of 2, whilst terms can be reduced mod 2 with a decreasing it can be seen that the order of subpolynomials drops rapidly during evaluation.
Returning to the worked example () = 3 + 3 + 22 + 43 and supposing that the input is
[1, 0, 1, 1] then (
The new input low bit is 1, so 1(
Next, the new input low bit is 0, so 11(0) = 2, the output low bit is 0 and the next subpolynomial is
(reducing modulo 2):
2 + 3 ↦→
=
shR(
Finally evaluate this at 1, giving 011(
As noted above, the bit-width drops by 1 with each subpolynomial, and the construction of the subpolynomials multiplies coeficients by powers of 2. This means that higher degree monomials disappear from subpolynomials quite rapidly. If in the original there is a monomial , noting that for each successive subpolynomial the monomial is multiplied by 2− 1, then in subpolynomial ...0 there will not be a monomial in when ( − 1) > − since the 2-adic valuation coeficient of in this subpolynomial will be greater than the bit-width of the bit-vector this subpolynomial is over. Rearranging the condition gives that > . Note that this is not independence of the subpolynomial from the higher degree monomial, since the constant is the result of the evaluation of the monomial for a previous subpolynomial.
Consider 3 + 3 + 22 + 43 + 24 + 36 + 27 evaluated over 32 bits. Then when > 372 , for example, = 5, the subpolynomial will have monomial 21+(5× 6)7 over 27 bits, hence will always evaluate to 0. Again consider the monomial with 2 and = 16. This will have coeficient 21+(16× 1) over 16 bits, hence again will always evaluate to 0. That is, the higher 16 bits of the output bit-vector can be described by a linear subpolynomial, and this be exploited when bit-blasting.
The same principle can be used to produce a compact bit-level encoding of a binary polynomial. The least significant bit of the output can be produced using single bit bvand and bvxor to evaluate multiplication and addition respectively. Then the subpolynomial can be computed using the least significant bit of the input, allowing the whole encoding to be generated iteratively. It is important to note that the coeficients in the subpolynomial will be symbolic expressions over the coeficient of the original binary polynomial and each of the lower input bits , − 1, . . . . So simplification requires symbolic rewriting not pure calculations. One of the necessary rewrite rules is not implemented in all solvers. Using lsb to denote (_ extract 0 0) and top to denote (_ extract w-1 1) and extend to denote (_ zero_extend w-2) the rule is: (top (bvadd x y)) = (bvadd (top x) (top y) (extend (bvand (lsb x) (lsb y))) This allows the subpolynomials to simplify away some terms while still correctly modelling the chains of carries that can occur in rare circumstances.
An additional advantage of handling symbolic coeficients is that the encoding can be applied recursively to multivariate polynomials if they can be put into the appropriate nested form, such as 5(1 + ) + (3 + 4 + 2) + 2(2 + 32). It remains an open question whether this is the most eficient approach to handling multivariate polynomials.
The ultimate aim of any novel encoding is to improve either the number of problems decided or run-time in one or more class of problems, while minimising any negative efects on other classes. Systemlevel evaluation of this sort can be challenging for a number of reasons – solver performance can be dependent on a large number of inter-related of factors, existing benchmark sets may not cover the class of problems improved by the encoding1 and even if system-level improvements are shown, it is not always clear why they occur or how it connects to the changes made.
Reasoning about binary polynomials have all of these problem. As a first step to evaluating the technique described in Section 4 the following will be shown using synthetic benchmarks: 1. Reduction (Section 2.2) and the subpolynomial encoding (Section 4) reduce the size of the bitblasted formulae.
2. They do not have an obvious negative efect on performance; simple problems remain simple. 1There is a social dynamic to this problem – if a class of problem is hard for current solvers, or thought to be hard, then it is likely that people will not “waste” time generating benchmarks for this class.
A benchmark generator has been written using the cvc5 API. It generates permutation polynomials of a given degree that have coeficients randomly chosen from bit-vectors of given width. These are used to create four SMT-LIB files with diferent encodings of the polynomial: 1. The original polynomial in canonical form using bvmul and bvadd so that the solver’s native simplification and encoding is used. 2. The original polynomial represented using the subpolynomial encoding. 3. The reduced polynomial expressed in canonical form so the solver’s native simplification and encoding is used.
4. The reduced polynomial represented using the subpolynomial encoding.
In each of these a single assertion requires that the output must be zero (i.e. finding a root of the polynomial). Permutation polynomials have exactly one root. Experiments with other families of polynomials suggest that there are classes of polynomial for which root finding is easier (in some case solvable with simplification alone). So permutation polynomials represent a “hardest case” for these techniques. 2
Bitwuzla [9] 0.7.0 is used as the leading bit-vector solver. Again this means any improvements are a lower bound, other solvers may have larger improvement. Evaluation was done using a 1.70GHz Intel Core i5-4210U, running Debian GNU/Linux 11. CPU time was limited to 60 seconds and memory limited to 1GB, although neither of these afected the results. Tables 1, 2 and 3 show the run time (in seconds) and the number of Boolean variables and clauses after bit-blasting for 8 bit, 16 bit and 32 bit polynomials over a range of degrees.
By comparing the original and reduced polynomials using the native encoding, it is possible to see that the reduction makes a significant diference to the variables and clauses used. The size of the original polynomial continues to rise as the degree rises. However the reduced polynomial encoding sizes stop rising when the bit-width reaches + 2, as predicted by the theoretical results in [2].
Comparing the native and subpolynomial encodings there is a significant reduction in the size of the encoding for all except the first few degrees in the larger bit-widths. In the most extreme cases 2The generator and benchmarks are available at https://github.com/martin-cs/subpolynomial-encoding Degree Time 2 0.00 3 0.01 4 0.02 5 0.02 6 0.03 7 0.04 8 0.04 9 0.04 10 0.06 11 0.07 12 0.05 13 0.05 14 0.06 15 0.09 16 0.10 17 0.07 18 0.09 19 0.09 20 0.13 21 0.08 22 0.10 23 0.19 24 0.10 25 0.12 26 0.15 27 0.20 28 0.14 29 0.16 30 0.25 31 0.14 32 0.25 the subpolynomial encodings are 20 times smaller. However typical cases are 3 to 10 times smaller. Critically this is achieved without significant increase in solving time.
Finally comparing the original and reduced polynomials using the subpolynomial encodings shows a very minimal benefit. This is likely because the higher degree terms that would definitely be removed during reduction would also be removed during the first few subpolynomial computation steps. However, notice the size of the subpolynomial encoding in terms of both variables and clauses is almost independent of the degree, reflecting that higher degree terms quickly drop out of subpolynomials.
This paper recaps previous results about the efective degree limit and reduction of binary (bit-vector) polynomials as well as proposing a new means of evaluation. Bit-blasting representations of binary polynomials using this evaluation method have been shown to be significantly more compact than Bitwuzla’s native encoding and not obviously detrimental to performance in synthetic benchmarks. Significant future work is needed to show that these encodings can produce system-level performance improvements. It will be necessary to extend subpolynomial evaluation to handle multivariate polynomials, to integrate this approach within a solver’s bit-blasting engine (including identifying / constructing polynomials from the solver input) and to identify suitable sets of “real world” benchmarks where Degree Time 2 0.01 3 0.04 4 0.07 5 0.14 6 0.10 7 0.31 8 0.16 9 0.36 10 0.38 11 0.20 12 0.32 13 0.43 14 0.31 15 0.32 16 0.66 17 0.46 18 0.64 19 0.57 20 0.74 21 0.76 22 0.91 23 0.52 24 1.24 25 1.27 26 0.88 27 1.26 28 1.31 29 0.74 30 1.49 31 1.19 32 1.53 33 1.08 34 0.84 35 0.89 36 1.52 37 1.04 38 0.99 40 1.85 42 1.10 44 1.53 46 2.48 48 1.42 50 2.70 52 2.81 54 1.73 56 2.11 58 3.17 60 1.80 62 1.91 64 2.38 reasoning about binary polynomials is central to the problem dificulty. This is first bit-blasting encoding of this kind and so further improvements are likely possible.