Introduction

The Boolean satisfiability problem (SAT) and polynomial system solving over a finite field (PSS) are two fundamental problems of propositional logic and computational commutative algebra, respectively. The decision versions of these problems, i.e., whether there exists a satisfying assignment for a Boolean formula or a common zero for a polynomial system over a finite field, are known to be NP-complete. In other words, both problems are in NP and reducible to each other in polynomial time. For practical reasons, the search versions of these problems are very important, i.e., to find one or all satisfying assignments, or to find one or all common zeros.

Efficient conversion methods for transforming a Boolean polynomial system to a SAT instance have been studied carefully. Some of them are tailored to algebraic attacks in cryptography (see [3] and [16]). Implementations of these conversions can be found for instance in the computer algebra systems Sage (see [21]) and ApCoCoA (see [20]). In this paper we focus on the reverse direction, i.e., the transformation of a SAT instance given by a set of clauses of a formula in conjunctive normal form (CNF) to a set of Boolean polynomials in algebraic normal form (ANF). The standard way to perform this conversion clause by clause has been known for a long time (see for instance [15]). However, more efficient methods which try to combine several clauses into one Boolean polynomial, preferably a short polynomial of low degree, have been considered only more recently and cursorily (see for instance [7]), mostly in the context of integrating Gröbner basis techniques into the various stages of a SAT solver.

Our motivation for studying more efficient methods for the CNF to ANF conversion derives from the attempt to solve large instances of the SAT or PSS problem which originate from cryptographic attacks. Rather than using some heuristics to call a Gröbner basis solver for supporting a SAT solver at selected points in the CDCL algorithm (for example, as in [22] and [10]), we are running a SAT solver and an algebraic solver in parallel and let them interchange information. For instance, for algebraic fault attacks targeting the Small-Scale AES cryptosystem, SAT clauses and Boolean polynomials have been derived both from a VDHL implementation of the circuit and from a functional model in [13]. It has been observed that a combination of the SAT solver antom (cf. [18]) and a border basis solver (cf. [14]) outperforms the individual solvers, if the communication between the processes provides clauses resp. Boolean polynomials which are most likely to aid the solver. Hence we are most interested in CNF to ANF conversions which yield many short linear or quadratic polynomials.

To achieve this goal we proceed as follows. In Section 2 we recall the basic definitions and notations regarding the ring of Boolean polynomials and propositional logic. In Section 3 we recall some conversion methods from ANF to CNF, and in Section 4 we briefly recap the standard conversion from CNF to ANF. Our main algorithm for the CNF to ANF conversion is developed in Section 5. The idea is to combine all clauses which share a certain number of variables (irrespective of their sign) into a block of clauses. Using an overlapping number m, we introduce an efficient algorithm for producing these m -blocks. Then, in the blockwise conversion algorithm, these m -blocks are converted individually using the standard conversion and for each converted block of polynomials we compute a reduced Gröbner basis. As it turns out, the Gröbner bases contain many more low degree polynomials than a standard conversion would have provided us with. We also show that the computation of these reduced Gröbner bases encompasses algebraic versions of the usual DPLL rules of inference (cf. Prop. 4).

The task of finding as many linear polynomials as possible in the ANF conversion of a block of clauses is examined further in Section 6. Based on the structure of the CNF transformation of a linear polynomial, we derive a combinatorial test which checks whether a block of clauses contains sufficiently many clauses that can be extended suitably to cover the transformation of a linear polynomial (cf. Prop. 7). This test is implemented in Algorithm 4. However, as Prop. 8 shows, these linear polynomials are found also by the calculation of the blockwise reduced Gröbner bases. Thus the blockwise conversion method given in Algorithm 3 automatically contains all linear polynomials which can be deduced from the set of clauses by simple combinatorial methods. An amusing consequence is that sometimes the double conversion from ANF to CNF and back is sufficient to solve the Boolean polynomial system, because the block-wise conversion algorithm produces enough linear polynomials to allow Gaußian elimination to work.

The final section contains some experiments in which we compare the new blockwise conversion algorithm to the standard CNF to ANF conversion. In many examples originating from cryptographic attacks and factorization problems, the new conversion method improves the input for the algebraic solver substantially.

Unless stated otherwise, we use the basic definitions and notation of [17].

Background

In this section we recall basic definitions and known results and introduce useful notation. In the following we let F 2 be the field of two elements and

F 2 [x 1 , . . . , x n ] a polynomial ring over F 2 . The ideal F = x 2 1 +x 1 , . . . , x 2 n +x n is called the field ideal, since it is the vanishing ideal of F n 2 . The ring B n = F 2 [x 1 , . . . ,

x n ]/ F is called the ring of Boolean polynomials in the indeterminates x 1 , . . . , x n . We assume that its elements are represented by polynomials whose support consists only of squarefree terms. Boolean polynomials in this shape are said to be in algebraic normal form (ANF). An arbitrary polynomial f can be transformed to ANF by computing its normal form NF F (f ) with respect to the field ideal. Notice that we use " + " instead of "⊕" for addition in F 2 .

Given a set S = {f 1 , . . . , f s } ⊆ B n , we define the set of F 2 -rational zeros of S by Z(S) = {a ∈ F n 2 | f (a) = 0 for all f ∈ S}. In fact, the set Z(S) does not depend on the particular choice of generators of the ideal I = f 1 , . . . , f s , but only on the ideal itself. Thus we can write Z(I) . Boolean polynomials correspond 1-1 to Boolean functions. The only Boolean polynomial f with Z(f ) = ∅ is the constant polynomial 1 .

Solvers that allow us to describe the set of zeros of a given ideal by algebraic techniques are referred to as algebraic solvers. We mention here the Boolean Gröbner Basis Algorithm [5, Ch. 2], the Boolean Border Basis Algorithm [14], the XL/XSL algorithm and its variants [8], and ElimLin [9]. For the (Boolean) Gröbner Basis Algorithm, the library PolyBoRi [6] and the FGb library [12] provide efficient actual implementations of such solvers. The basic principle of algebraic solvers is to generate new polynomials in the ideal and simplify the newly derived polynomials by the old ones. For the theory of Boolean Gröbner bases, we refer to [5,Ch. 2]. Every ideal I ⊆ B n can be represented by an ideal I ⊆ F 2 [x 1 , . . . , x n ] such that F ⊆ I . Hence Boolean Gröbner bases correspond to Gröbner bases of ideals containing the field equations.

Every propositional logic formula ϕ can be encoded in conjunctive normal form (CNF). A clause is a set of literals, i.e. logical variables X i or their negation Xi . A set of clauses

C = {L 1,1 , . . . , L 1,n1 }, . . . , {L k,1 , . . . , L k,n k } corresponds to the logic formula ϕ = (L 1,1 ∨• • •∨L 1,n1 )∧• • •∧(L k,1 ∨• • •∨L k,n k ) .

We always assume that ϕ is in CNF and given by its set of clauses C . This allows us to identify ϕ and C . The algorithms that search for a satisfying assignment for C are called SAT solvers. In order to find the whole solution space, so-called #SAT solvers are used. Most modern SAT solvers are based on a CDCL procedure, i.e. on resolution with the addition of clause learning. They generate new clauses, called conflict clauses, that guide the computation. Together with non-chronological backtracking and highly optimized data structures, they are very powerful tools. Two standard implementations of the SAT algorithm are MiniSAT [11] and Glucose [1].

To distinguish variables in a Boolean polynomial ring and in formulae, we use lower-case letters for variables in Boolean polynomials and capital letters for the corresponding logical variables. Moreover, we identify True ≡ 1 and False ≡ 0 . Definition 1. Let S ⊆ B n be a set of Boolean polynomials and C a set of clauses in the logical variables X 1 , . . . , X n . We say that C is a logical representation of S , resp. S is an algebraic representation of C , if and only if

SAT(C) = Z(S) .

The algebraic representation of S is not unique in general. On the other hand, if #S = 1 , the representation is unique. Namely, one Boolean polynomial f represents the unique Boolean function F n 2 → F 2 mapping a → 0 if a ∈ SAT(C) and a → 1 otherwise. In this case, we say that f is the standard algebraic representation of C .

Conversions from ANF to CNF

First of all, let us discuss what kinds of ANF systems are well suited to converting them to SAT. Note that if the system is rather dense, it is probably better to solve it by algebraic solvers or even by brute force. A typical example where algebraic solvers outperform SAT solvers is solving a dense linear system. On the other hand, the memory consumption of SAT solvers is kept under control, and therefore they tend to be faster for sparse constraint inputs, for which algebraic solvers may have a huge space consumption. (For more details and experiments, see [2], Ch. 13.)

In this section we recall some efficient conversion methods for a set of Boolean polynomials in ANF (i.e., XOR of ANDs) to a Boolean formula in CNF (i.e., AND of ORs). There are basically two types of such conversions. Both of them convert only one Boolean polynomial at a time. The first conversion method does not introduce new auxiliary variables, creating a sparse representation, whereas the second one does and results in a dense representation.

The sparse conversion is truth-based and uses the assumption that the input polynomials are rather sparse (i.e. they do not have many terms and variables). Thus one can go trough all possible assignments for all logical variables contained in the polynomial to construct the sparse CNF.

Example 1. Consider the truth table of the polynomialf (x 1 , x 2 ) = x 1 x 2 +x 2 +1 . x 1 x 2 f 0 0 1 0 1 0 1 0 1 1 1 1

For each assignment that yields True, we construct one clause that eliminates this particular assignment. Thus the set of clauses C = {X 1 , X 2 }, { X1 , X 2 }, { X1 , X2 } is the logical representation of the polynomial f . Note that the set {x 1 , x 2 + 1} is an algebraic representation of C as well, so the representations are not uniquely determined.

Dense conversion methods (see [3], [16]) introduce new variables. Foremost, the polynomial f ∈ B n is linearized. For each of its terms of degree greater than one, we introduce a new auxiliary indeterminate t and encode the resulting binomial in CNF. E.g., we convert x 1 x 2 x 3 by encoding t + x 1 x 2 x 3 to the clauses {X 1 , T }, {X 2 , T }, {X 3 , T } , { X1 , X2 , X3 , T } . After this step, we are left with (possibly long) linear polynomials. We split them into smaller ones by introducing further auxiliary indeterminates according to a predefined cutting number r . To the resulting shorter linear polynomials we apply the sparse conversion.

Example 2. Let r = 3 . We cut the linear polynomial x 1 + x 2 + • • • + x 5 into two polynomials x 1 + x 2 + x 3 + y and y + x 4 + x 5 . Note that we have introduced one new indeterminate y here. For instance, when we convert x 1 + x 2 + x 3 + x 4 , we get the clauses

{ X1 , X 2 , X 3 , X 4 }, {X 1 , X2 , X 3 , X 4 }, {X 1 , X 2 , X3 , X 4 }, {X 1 , X 2 , X 3 , X4 }, { X1 , X2 , X3 , X 4 }, { X1 , X2 , X 3 , X4 }, { X1 , X 2 , X3 , X4 }, {X 1 , X2 , X3 , X4 }.

Both conversions suffer from the problem that breaking the XOR structure in the ANF tends to introduce many auxiliary indeterminates or many new clauses.

The Standard Conversion from CNF to ANF

The standard conversion from CNF to ANF converts each clause of C to one Boolean polynomial. It has been known for a long time (cf. [15]). The detailed description is given in Algorithm 1.

Proposition 1. Algorithm 1 outputs a system of Boolean polynomials S such that S is an algebraic representation of C .

Proof. Let c = {L 1 , L 2 , . . . , L m } be a clause of C . The assignment (a 1 , . . . , a n ) ∈ F n 2 satisfies c if and only if the polynomial f = 1 • • • m vanishes at the point (a 1 , . . . , a n ) , where i = x i + 1 for L i = X i and i = x i for L i = Xi .

Let us apply this algorithm to a concrete case.

Algorithm 1 (Standard CNF to ANF Conversion)

Input: A set of clauses C in logical variables X 1 , . . . , X n . Output: A set S ⊆ B n such that S is an algebraic representation of C .

1: S := ∅ 2: foreach c in C do 3: f := 1 4: foreach L in c do 5: if L = Xi is positive then 6: f := f • (xi + 1) 7: else if L = Xi is negative then 8: f := f • (xi) 9:

end if 10:

end foreach 11:

S := S ∪ {f } 12: end foreach 13: return S Example 3. Given the set of clauses {{X 1 , X 2 }, { X1 , X 2 , X 3 }, {X 4 , X 5 }, {X 1 , X2 , X 3 }, { X1 , X2 , X3 }, {X 4 , X5 } , the Standard CNF to ANF Conversion yields the following results: {X 1 , X 2 } → x 1 x 2 + x 1 + x 2 + 1 { X1 , X 2 , X 3 } → x 1 x 2 x 3 + x 1 x 2 + x 1 x 3 + x 1 {X 4 , X 5 } → x 4 x 5 + x 4 + x 5 + 1 {X 1 , X2 , X 3 } → x 1 x 2 x 3 + x 1 x 2 + x 2 x 3 + x 1 { X1 , X2 , X3 } → x 1 x 2 x 3 {X 4 , X5 } → x 4 x 5 + x 5

Clearly, Algorithm 1 performs at most n • #C multiplications in B n . Thus it is of polynomial time complexity. Notice that its output for a single input clause c is the standard algebraic representation of c. Moreover, deg(f ) equals the length of the clause c in Step 12 of the algorithm. Hence even a small set of clauses may be converted to a polynomial system containing high-degree polynomials. The degree and the length of the support of these polynomials can be viewed as an indicator of their usefulness. It follows that such a conversion does, in general, not give an encoding which is useful for further applications. In particular, converting a simple Boolean system S to CNF using the sparse strategy and back to polynomials by Algorithm 1, gives us a rather denser and higher-degree system Ŝ . Even if the computation of a Gröbner basis of the ideal S may be done in seconds, a Gröbner basis of the ideal Ŝ can take hours to compute.

A Blockwise Conversion from CNF to ANF

Let C be a set of clauses representing a propositional logic formula in CNF. First of all, we group certain clauses in C together using the following definitions. The elements of the set B returned by Algorithm 2 will be called the mblocks of C . Let us apply Algorithm 2 in some easy cases.

Example 4. Let C = {c 1 , c 2 , c 3 } with c 1 = {X 1 , X 2 , X 3 , X 4 } , c 2 = {X 1 , X 2 }

and c 3 = {X 3 , X 4 } , and let m = 2 . Then the entire set C is one 2 -block. Notice that this block does not correspond to a complete subgraph of G m,C , because the edge (c 2 , c 3 ) is missing.

Example 5. In the setting of Example 3, Algorithm 2 calculates the following two 2-blocks.

{X 1 , X 2 } { X1 , X 2 , X 3 } {X 4 , X 5 } {X 1 , X2 , X 3 } { X1 , X2 , X3 } {X 4 , X5 } →     {X 1 , X 2 } { X1 , X 2 , X 3 } {X 1 , X2 , X 3 } { X1 , X2 , X3 }     , {X 4 , X 5 } {X 4 , X5 }

Let σ be a degree compatible term ordering. We say that a set of Boolean polynomials G ⊆ B n is LT σ -interreduced if LT σ (g) = LT σ (g ) for all g, g ∈ G with g = g . Given an arbitrary set of Boolean polynomials G ⊆ B n , we can LT σ -interreduce G via Gaußian elimination on the coefficient matrix of G, where its columns are sorted from biggest to the smallest term w.r.t. σ . Now we are ready to describe the main Algorithm 3.

Algorithm 3 (Blockwise CNF to ANF Conversion)

Input: A set of clauses C in logical variables X 1 , . . . , X n , a degree compatible term ordering σ , and an overlapping number m ∈ N. Output: A set S σ,m ⊆ B n such that S σ,m is an algebraic representation of C . Requires: Algorithm 1 and 2, a reduced Boolean Gröbner basis algorithm. Let G be the reduced Boolean σ -Gröbner basis of the ideal Q , i.e., the reduced Boolean Gröbner basis with respect to the term ordering σ . 7:

S := S ∪ G 8: end foreach 9: Let Sσ,m be an LTσ -interreduced F2 -basis of S F 2 such that its coefficient matrix w.r.t. σ is in reduced row echelon form. 10: return Sσ,m

It is difficult to give a meaningful upper bound for the time complexity of this algorithm, since it involves a number of Gröbner basis calculations. As we shall see in the next section, if one of the sets in B contains a complete signed set of clauses (see Definition 3), the conversion will contain a linear polynomial. In this case, the corresponding Gröbner basis will be found rather quickly. As one can infer from the tables in the last section, this happens a lot in practically relevant cases. But, of course, it is clear that one can construct special sets of clauses for which the Gröbner basis calculation is particularly expensive.

    {X 1 , X 2 } → x 1 x 2 + x 1 + x 2 + 1 { X1 , X 2 , X 3 } → x 1 x 2 x 3 + x 1 x 2 + x 1 x 3 + x 1 {X 1 , X2 , X 3 } → x 1 x 2 x 3 + x 1 x 2 + x 2 x 3 + x 1 { X1 , X2 , X3 } → x 1 x 2 x 3     → x 2 x 3 + x 2 + x 3 + 1 x 1 + x 2 + x 3 {X 4 , X 5 } → x 4 x 5 + x 4 + x 5 + 1 {X 4 , X5 } → x 4 x 5 + x 5 → x 4 + 1

As we can see, the output is a set of three polynomials of degrees 1,1,2 instead of the six polynomials of degrees 2,2,2,3,3,3 in Example 3.

In the following proposition we study Step 6 of Algorithm 3 in more detail. Its Claims (1)-( 4) are algebraic versions of the one-literal, subsumption, cleanup, and resolution rules of DPLL. In this sense, the Gröbner basis algorithm can be interpreted as performing simple logical reasoning. Proposition 4. In the setting of Algorithm 3, let B = {c 1 , . . . , c k } be a set of clauses. Let Q = {q 1 , . . . , q k } be the set of Boolean polynomials such that q i is the standard algebraic representation of c i for i = 1, . . . , k . Let G be the reduced Boolean σ -Gröbner basis of the ideal I = Q .

(1) Let c i , c j ∈ B be clauses such that c i is a proper subclause of c j . Then G is equal to the reduced Boolean σ -Gröbner basis of Q \ {q j } .

(2) Let L be a literal and assume that c j = {L} is an element of B . Let {q i1 , . . . , q is } be the set of all clauses in B different from q j and containing the literal L. Then G is the reduced Boolean σ -Gröbner basis of Q \ {q i1 , . . . , q is } . (3) Let c i ∈ B be of the form c i = c ∪{X j , Xj } for some clause c and a logical variable X j . Then G is the reduced Boolean σ -Gröbner basis of Q \ {q i } . (4) Assume that c i , c j ∈ B satisfy c i = w ∪ {X e } and c j = w ∪ { Xe } for some logical variable X e and clauses w, w . Let r = w ∪ w be the resolvent of c and c on the variable X e . Then the standard algebraic representation of r is the S-polynomial of q i , q j . ( 5) We have

SAT(B) = ∅ if only if G = {1}. (6) Let #B ≥ 2 .

If there exists a clause c j ∈ B such that var(c ) ⊆ var(c j ) holds for all c ∈ B , then we have max{deg(g) | g ∈ G} < max{deg(q) | q ∈ Q} . (7) Let f ∈ I be such that there exists a clause c for which f is the standard algebraic representation of c. If there exists a Boolean polynomial g ∈ G such that LT σ (f ) = LT σ (g), then f = g .

Proof.

(1) From the inclusion c i ⊂ c j , we know that q j is a multiple of q i . Hence q j is reduced to zero by q i and the claim follows.

(2) All polynomials in {q i1 , . . . , q is } are multiples of q j and thus are reduced to zero. (3) The standard algebraic representation of c i is q i = x j (x j + 1)f for some variable x j and a polynomial f . Thus the Boolean polynomial q i satisfies q i = (x 2 j + x j )f = 0 in B n and the claim follows. (4) The standard algebraic representation of c i resp. c j is q i = x e f resp. q j = (x e + 1)g for some polynomials f, g . The S-polynomial of q i , q j is equal to f g = g(x e f ) + f (x e + 1)g . ( 5) We know that the variety of Q over the algebraic closure of F 2 is equal to Z(Q) , because we assume that the field equations are included in the ideal. Hence the claim follows from the strong version of Hilbert's Nullstellensatz. (6) If q j is the only polynomial with the maximal degree in Q, then there exists c i ∈ B such that c i ⊂ c j and we apply Claim (1). If there is another q ∈ Q with the maximal degree in Q different from q j , then LT σ (q) = LT σ (q j ) . Hence we drop the degree at least by one after the LT-reduction. (7) We have f = j=1 (x ij + a j ) for some a j ∈ F 2 and for some number .

Because LT σ (f ) = LT σ (g) , we know that LT σ (f ) is minimal w.r.t. division in LT σ (I) . All terms in f divide LT σ (f ) , and so f can not be further reduced. Thus f is contained in some reduced Boolean σ -Gröbner basis of the ideal I . The claim follows form the uniqueness of the reduced Boolean σ -Gröbner basis.

Notice that Claim (6) can also be found in [5, Thm. 5.3.5.].

Conversion to Linear Polynomials

The most valuable polynomials for algebraic solvers in the result of a CNF to ANF conversion algorithm are the linear ones. Therefore we now focus on the problem of identifying sets of clauses containing a linear polynomial in their algebraic representation. Definition 3. A set of clauses, all of which have the same length, which consists of all possible clauses with either only positive or only negative sign is called a complete signed set of clauses.

A complete signed set of clauses forms a complete subgraph of the graph G ,C (see the definition in the proof of Proposition 2) having only positive, or only negative clauses of length as nodes. A complete signed set of clauses of length consists of 2 −1 clauses. Proposition 5. Let K be a complete signed set of clauses with positive (resp. negative) sign and var(K) = {X i1 , . . . , X i }. Then

x i1 + • • • + x i + 1 (resp. x i1 + • • • + x i ) is the standard algebraic representation of K . Proof. Let K be the sparse conversion of f = x i1 + • • • + x i + 1 .

From the truth table of f it is easy to see that K is a complete signed set of clauses with positive sign in the variables var(K) . Complete signed sets of clauses with positive sign are uniquely determined by their set of variables. Thus we get K = K . The negative case follows analogously. Proof. Claim (a) can be easily proven by comparing a truth table for ϕ and (ϕ ∨ ψ) ∧ (ϕ ∨ ψ) . The other claims are immediate consequences of (a).

The following example illustrates this proposition.

Example 7. Let B = {X 1 , X 2 }, { X1 , X 2 , X 3 }, {X 1 , X2 , X 3 }, { X1 , X2 , X3 } . The first clause in B is equivalent to the two clauses {X 1 , X 2 , X 3 } , {X 1 , X 2 , X3 } .

In view of this, we have covered all four possible combinations for negative signed clauses of length 3 . Indeed, Algorithm 3 converts B into x 1 + x 2 + x 3 and x 2 x 3 + x 2 + x 3 + 1 .

Proposition 6 leads to the following combinatorial test for checking whether a set of clauses B converts to a linear polynomial. B − := ∅ 5:

for j = 1, . . . , k do 6:

B + := B + ∪ B + j,V 7: B − := B − ∪ B − j,V

8: end for 9:

if #B + = 2 −1 then 10:

L := L ∪ {xi 1 + • • • + xi + 1} 11: end if 12: if #B − = 2 −1 then 13: L := L ∪ {xi 1 + • • • + xi } 14:

end if 15: end foreach 16: Let L be an LTσ -interreduced F2 -basis of L (2) Assume that Algorithm4( C ) has discovered a set of clauses K which contains a complete signed block after extension. Using Algorithm2(C , m), compute a pair (B, T ) . If # var(K) = 1 , then the corresponding linear polynomial will be derived from a clause in T and we are done. If # var(K) ≥ 2 , then K will appear in one B ∈ B , and we can use (1) .

During our experiments, we found that conversion of a Boolean system to CNF and back to ANF may give us enough linearly independent linear polynomials to solve the initial system S . Note that having n linearly independent linear polynomials in the ideal S ⊂ B n is enough to derive the unique solution of the system by Gaußian elimination. We observed this behavior for the polynomials representing Small-scale AES encryption AES-1-1-1-4 and AES-2-1-1-4. The polynomials can be found in Sage [21]. For bigger examples, this is usually not the case. On the other hand, one frequently gains additional linear polynomials in the ideal by this technique. It is made explicit in Algorithm 5.

Experiments

In this section we examine the efficiency of the proposed improvements of the CNF to ANF conversion. In Table 1 we compare Algorithm 1 with Algorithm 3 w.r.t. the degree of the resulting algebraic representations.

The tests have been executed on a compute server having a 3.00 GHz Intel(R) Xeon(R) CPU E5-2623 v3 and a total of 48 GB RAM. All algorithms in this paper were prototypically implemented in python v2.7 using the PolyBoRi library [6] integrated in Sage [21] for the Gröbner basis computations. We choose the specific mid-size instances from the following benchmark suites: the logical representations of the encryption of the Small-scale AES cipher [13] and factoring of integers [4] Table 1 provides information about the number of variables and the number of clauses contained in the CNF instance, as well as the total number of linear, quadratic and higher degree (i.e., greater than 2) polynomials produced by Algorithms 1 and 3. We use σ = degrevlex and m = 2 . The later parameter performed the best (see Proposition 8), because it does not create big blocks B c in Algorithm 2 that are too hard for the Gröbner basis computation. On the other hand, choosing m ≥ 3 does not make sense in most examples, because the CNF instances usually contain many clauses of length 3.

From the results in Table 1 we clearly see that the algebraic representation given by Algorithm 3 produces lower degree polynomials than the one by Algorithm 1. While Algorithm 1 usually produces only very few linear polynomials, the table shows that Algorithm 3 tends to return enough linear polynomials to eliminate approximately one third of all indeterminates. Moreover, we note that Algorithm 3 almost completely avoided to produce polynomials of degree ≥ 3 .

In our experiments, the computation of the reduced Gröbner bases of the conversions of the block B c did not pose problems. If necessary, one could calculate them in parallel. Both algorithms need extra time for the setup of the Boolean rings. This could be a problem for larger CNFs having thousands of variables. It can be overcome by defining local Boolean rings for each B c and then rewriting the local variables in B c to their global names. Note that # var(B c ) tends to be much smaller than # var(C) . Moreover, caching of the standard representations of short clauses is possible. Polynomials of type l i=1 (x i + a i ) can be precomputed and stored in ANF for small values of . Then the corresponding values a i ∈ F 2 are substituted for a given clause. Proposition 4 states that Algorithm 3 does simple logical reasoning, e.g., it applies the resolution rule to certain subformulae. Thus it tends to produce lower degree polynomials. One possible enhancement would be to run a SAT solver on a given set of clauses C for a while, and then to apply Algorithm 3 on C together with the newly found clauses (e.g., conflict clauses). We believe that this would produce even more low degree polynomials.