On Conversions from CNF to ANF Jan Horáček and Martin Kreuzer Faculty of Informatics and Mathematics University of Passau, D-94030 Passau, Germany Jan.Horacek@uni-passau.de, Martin.Kreuzer@uni-passau.de Abstract. In this paper we discuss conversion methods from the con- junctive normal form (CNF) to the algebraic normal form (ANF) of a Boolean function. Whereas the reverse conversion has been studied be- fore, the CNF to ANF conversion has been achieved predominantly via a standard method which tends to produce many polynomials of high degree. Based on a block-building mechanism, we design a new block- wise algorithm for the CNF to ANF conversion which is geared towards producing fewer and lower degree polynomials. In particular, we look for as many linear polynomials as possible in the converted system and check that our algorithm finds them. Experiments show that the ANF produced by our algorithm outperforms the standard conversion in “real life” examples originating from cryptographic attacks. Keywords: conjunctive normal form, algebraic normal form, Boolean polyno- mial, Boolean Gröbner basis, SAT solving 1 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 direc- tion, 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, 1 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 infor- mation. 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 communi- cation 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 proposi- tional 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 pro- vided 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 con- version 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 combi- natorial 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- 2 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 prob- lems, the new conversion method improves the input for the algebraic solver substantially. Unless stated otherwise, we use the basic definitions and notation of [17]. 2 Background In this section we recall basic definitions and known results and introduce useful notation. In the following we let F2 be the field of two elements and F2 [x1 , . . . , xn ] a polynomial ring over F2 . The ideal F = hx21 +x1 , . . . , x2n +xn i is called the field ideal, since it is the vanishing ideal of Fn2 . The ring Bn = F2 [x1 , . . . , xn ]/hF i is called the ring of Boolean polynomials in the indeterminates x1 , . . . , xn . 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 al- gebraic normal form (ANF). An arbitrary polynomial f can be transformed to ANF by computing its normal form NFF (f ) with respect to the field ideal. Notice that we use “ + ” instead of “⊕” for addition in F2 . Given a set S = {f1 , . . . , fs } ⊆ Bn , we define the set of F2 -rational zeros of S by Z(S) = {a ∈ Fn2 | 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 = hf1 , . . . , fs i, 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 ⊆ Bn can be represented by an ideal I 0 ⊆ F2 [x1 , . . . , xn ] such that F ⊆ I 0 . 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 Xi or their negation X̄i . A set of clauses C = {L1,1 , . . . , L1,n1 }, . . . , {Lk,1 , . . . , Lk,nk } corresponds to the logic formula ϕ = (L1,1 ∨· · ·∨L1,n1 )∧· · ·∧(Lk,1 ∨· · ·∨Lk,nk ) . We always assume that ϕ is in CNF and given by its set of clauses C . This allows us to identify ϕ and C . 3 Next we define the set of satisfying assignments for a given set of clauses C in n logical variables by SAT(C) = a ∈ {False, True}n | C(a) evaluates to True .  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 reso- lution 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 ⊆ Bn be a set of Boolean polynomials and C a set of clauses in the logical variables X1 , . . . , Xn . We say that C is a logical repre- sentation 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 Fn2 → F2 mapping a 7→ 0 if a ∈ SAT(C) and a 7→ 1 otherwise. In this case, we say that f is the standard algebraic representation of C . 3 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 vari- ables). Thus one can go trough all possible assignments for all logical variables contained in the polynomial to construct the sparse CNF. 4 Example 1. Consider the truth table of the polynomial f (x1 , x2 ) = x1 x2 +x2 +1 . x1 x2 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 = {X1 , X2 }, {X̄1 , X2 }, {X̄1 , X̄2 } is the logical representation of the polynomial f . Note that the set {x1 , x2 + 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 ∈ Bn is linearized. For each of its terms of degree greater than one, we introduce a new auxiliary indeterminate t and encode the resulting bi- nomial in CNF. E.g., we convert x1 x2 x3 by encoding t + x1 x2 x3 to the clauses {X1 , T̄ }, {X2 , T̄ }, {X3 , T̄ } , {X̄1 , X̄2 , X̄3 , T } . After this step, we are left with (possibly long) linear polynomials. We split them into smaller ones by introduc- ing 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 x1 + x2 + · · · + x5 into two polynomials x1 + x2 + x3 + y and y + x4 + x5 . Note that we have introduced one new indeterminate y here. For instance, when we convert x1 + x2 + x3 + x4 , we get the clauses {X̄1 , X2 , X3 , X4 }, {X1 , X̄2 , X3 , X4 }, {X1 , X2 , X̄3 , X4 }, {X1 , X2 , X3 , X̄4 }, {X̄1 , X̄2 , X̄3 , X4 }, {X̄1 , X̄2 , X3 , X̄4 }, {X̄1 , X2 , X̄3 , X̄4 }, {X1 , X̄2 , X̄3 , X̄4 }. Both conversions suffer from the problem that breaking the XOR structure in the ANF tends to introduce many auxiliary indeterminates or many new clauses. 4 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 = {L1 , L2 , . . . , Lm } be a clause of C . The assignment (a1 , . . . , an ) ∈ Fn2 satisfies c if and only if the polynomial f = `1 · · · `m vanishes at the point (a1 , . . . , an ) , where `i = xi + 1 for Li = Xi and `i = xi for Li = X̄i . t u Let us apply this algorithm to a concrete case. 5 Algorithm 1 (Standard CNF to ANF Conversion) Input: A set of clauses C in logical variables X1 , . . . , Xn . Output: A set S ⊆ Bn 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 = X̄i 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 {{X1 , X2 }, {X̄1 , X2 , X3 }, {X4 , X5 }, {X1 , X̄2 , X3 }, {X̄1 , X̄2 , X̄3 }, {X4 , X̄5 } , the Standard CNF to ANF Conversion yields the following results: {X1 , X2 } → x1 x2 + x1 + x2 + 1 {X̄1 , X2 , X3 } → x1 x2 x3 + x1 x2 + x1 x3 + x1 {X4 , X5 } → x4 x5 + x4 + x5 + 1 {X1 , X̄2 , X3 } → x1 x2 x3 + x1 x2 + x2 x3 + x1 {X̄1 , X̄2 , X̄3 } → x1 x2 x3 {X4 , X̄5 } → x4 x5 + x5 Clearly, Algorithm 1 performs at most n · #C multiplications in Bn . 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 hSi may be done in seconds, a Gröbner basis of the ideal hŜi can take hours to compute. 5 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. 6 Definition 2. (a) The set of variables Xi such that Xi or X̄i is contained in one of the clauses of C is denoted by var(C) and is called the set of variables of C . (b) We say c ∈ C has positive (resp. negative ) sign if the number of negative literals is an even (resp. odd) number. (c) We define the length of a clause c ∈ C as the cardinality #c. (d) Let c, c0 ∈ C . A number m ≥ 1 such that # var(c) ∩ var(c0 ) ≥ m is called an overlapping number of c and c0 . Given a number m, Algorithm 2 decomposes a set of clauses C into blocks Bc for c ∈ C such that m is an overlapping number of c with every clause in Bc . Algorithm 2 (Building m-Blocks) Input: A set of clauses C , an overlapping number m ∈ N . Output: A set of subsets B of C and a subset T of C such that for B ∈ B with #B ≥ 2 and for every b ∈ B , there exists an element b0 ∈ B \ {b} with 0 the S property  that m is an overlapping number for b and b , and such that B∈B B ∪ T = C and every clause in T contains less than m literals. 1: foreach  c in C do Bc := c0 ∈ C | # var(c) ∩ var(c0 ) ≥ m  2: 3: end foreach 4: B0 := {Bc | c ∈ C, Bc 6= ∅} the set of maximal elements of B0 w.r.t. inclusion. 5: Let B be S 6: T := C \ c∈C Bc 7: return (B, T ) Notice that some clauses in C may not be included in the set B produced by Algorithm 2. This happens when the length of a clause is less than m . Such clauses are returned in the set T . Furthermore, the cardinality of the set of clauses contained in B ∪ T may be greater than #C . The cardinality is at least equal to #C , because every c ∈ C is contained either in the set Bc in B , or c is put into T in Step 6. Moreover, we note that Algorithm 2 performs at most #C iterations of the foreach loop, at most #C 2 intersections in Step 2, and at #B  most 2 comparisons in Step 5. Hence this algorithm has a polynomial time complexity. Proposition 2. The output of Algorithm 2 is uniquely determined. Proof. The sets in B are related to the following graph. For m ∈ N, we define an undirected graph Gm,C which has C as vertices and for which  two distinct clauses c, c0 ∈ C form an edge if and only if # var(c) ∩ var(c0 ) ≥ m . Clearly, Step 2 of Algorithm 2 computes the closed neighborhood of a vertex c of Gm,C , i.e. the set of all vertices connected to c by an edge. Then Step 5 selects the maximal neighborhoods w.r.t. inclusion. This shows that the output of Algo- rithm 2 is uniquely determined by C and m , and does not depend on the order in which the clauses c are selected in Step 1. t u 7 The elements of the set B returned by Algorithm 2 will be called the m- blocks of C . Let us apply Algorithm 2 in some easy cases. Example 4. Let C = {c1 , c2 , c3 } with c1 = {X1 , X2 , X3 , X4 } , c2 = {X1 , X2 } and c3 = {X3 , X4 } , 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 Gm,C , because the edge (c2 , c3 ) is missing. Example 5. In the setting of Example 3, Algorithm 2 calculates the following two 2-blocks. {X1 , X2 }   {X̄1 , X2 , X3 } {X1 , X2 }   {X4 , X5 }  {X̄1 , X2 , X3 }  {X4 , X5 } →  , {X1 , X̄2 , X3 }  {X1 , X̄2 , X3 }  {X4 , X̄5 } {X̄1 , X̄2 , X̄3 } {X̄1 , X̄2 , X̄3 } {X4 , X̄5 } Let σ be a degree compatible term ordering. We say that a set of Boolean polynomials G ⊆ Bn is LTσ -interreduced if LTσ (g) 6= LTσ (g 0 ) for all g, g 0 ∈ G with g 6= g 0 . Given an arbitrary set of Boolean polynomials G ⊆ Bn , 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 X1 , . . . , Xn , a degree compatible term ordering σ , and an overlapping number m ∈ N. Output: A set Sσ,m ⊆ Bn such that Sσ,m is an algebraic representation of C . Requires: Algorithm 1 and 2, a reduced Boolean Gröbner basis algorithm. 1: S 0 := ∅ 2: Using Algorithm2( S C , m ), compute a pair (B, T ) . 3: B := B ∪ t∈T {t} 4: foreach B in B do 5: Q := Algorithm1( B ) 6: Let G be the reduced Boolean σ -Gröbner basis of the ideal hQi , i.e., the reduced Boolean Gröbner basis with respect to the term ordering σ . 7: S 0 := S 0 ∪ G 8: end foreach 9: Let Sσ,m be an LTσ -interreduced F2 -basis of hS 0 iF2 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 8 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. Proposition 3. The output of Algorithm 3 is an algebraic representation of C and is uniquely determined by σ and m . Proof. First S we prove S that  Sσ,m is an algebraic representation of C . In Step 3 we have B∈B c∈B c = C , because every c ∈ C is contained either in the set Bc in B , or c is put into T in Step 6 of Algorithm 2. We know that Q is an algebraic representation of B ∈ B in Step 5 by Proposition 1. Furthermore, G is an algebraic representation of B as well, because hQi = hGi . Clearly, if G1 resp. G2 are algebraic representations of B1 resp. B2 , then G1 ∪ G2 is an algebraic representation of B1 ∪ B2 . Thus S 0 is an algebraic representation of C in Step 9. LTσ -interreduction does not change the set of zeros, and therefore Sσ,m is an algebraic representation of C . By Proposition 2 we know that the set B in Step 3 is uniquely determined. The reduced Boolean σ -Gröbner basis of the ideal hQi in Step 6 is unique, and so is the basis in Step 9. t u Example 6. Let us apply Algorithm 3 in the setting of Example 3.   {X1 , X2 } → x1 x2 + x1 + x2 + 1  {X̄1 , X2 , X3 } → x1 x2 x3 + x1 x2 + x1 x3 + x1  x2 x3 + x2 + x3 + 1  {X1 , X̄2 , X3 } → x1 x2 x3 + x1 x2 + x2 x3 + x1  → x1 + x2 + x3   {X̄1 , X̄2 , X̄3 } → x1 x2 x3   {X4 , X5 } → x4 x5 + x4 + x5 + 1 → x4 + 1 {X4 , X̄5 } → x4 x5 + x5 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, clean- up, 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 = {c1 , . . . , ck } be a set of clauses. Let Q = {q1 , . . . , qk } be the set of Boolean polynomials such that qi is the standard algebraic representation of ci for i = 1, . . . , k . Let G be the reduced Boolean σ -Gröbner basis of the ideal I = hQi. (1) Let ci , cj ∈ B be clauses such that ci is a proper subclause of cj . Then G is equal to the reduced Boolean σ -Gröbner basis of hQ \ {qj }i. 9 (2) Let L be a literal and assume that cj = {L} is an element of B . Let {qi1 , . . . , qis } be the set of all clauses in B different from qj and con- taining the literal L. Then G is the reduced Boolean σ -Gröbner basis of hQ \ {qi1 , . . . , qis }i. (3) Let ci ∈ B be of the form ci = c0 ∪{Xj , X̄j } for some clause c0 and a logical variable Xj . Then G is the reduced Boolean σ -Gröbner basis of hQ \ {qi }i. (4) Assume that ci , cj ∈ B satisfy ci = w ∪ {Xe } and cj = w0 ∪ {X̄e } for some logical variable Xe and clauses w, w0 . Let r = w ∪ w0 be the resolvent of c and c0 on the variable Xe . Then the standard algebraic representation of r is the S-polynomial of qi , qj . (5) We have SAT(B) = ∅ if only if G = {1}. (6) Let #B ≥ 2 . If there exists a clause cj ∈ B such that var(c0 ) ⊆ var(cj ) holds for all c0 ∈ 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 ci ⊂ cj , we know that qj is a multiple of qi . Hence qj is reduced to zero by qi and the claim follows. (2) All polynomials in {qi1 , . . . , qis } are multiples of qj and thus are reduced to zero. (3) The standard algebraic representation of ci is qi = xj (xj + 1)f for some variable xj and a polynomial f . Thus the Boolean polynomial qi satisfies qi = (x2j + xj )f = 0 in Bn and the claim follows. (4) The standard algebraic representation of ci resp. cj is qi = xe f resp. qj = (xe + 1)g for some polynomials f, g . The S-polynomial of qi , qj is equal to f g = g(xe f ) + f (xe + 1)g . (5) We know that the variety of Q over the algebraic closure of F2 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 qj is the only polynomial with the maximal degree in Q, then there exists ci ∈ B such that ci ⊂ cj and we apply Claim (1). If there is another q ∈ Q with the maximal degree in Q different from qj , then LTσ (q) = LTσ (qj ) . Hence we drop Q the degree at least by one after the LT-reduction. ` (7) We have f = j=1 (xij + aj ) for some aj ∈ F2 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. t u Notice that Claim (6) can also be found in [5, Thm. 5.3.5.]. 6 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 10 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) = {Xi1 , . . . , Xi` }. Then xi1 + · · · + xi` + 1 (resp. xi1 + · · · + xi` ) is the standard algebraic representation of K . Proof. Let K 0 be the sparse conversion of f = xi1 + · · · + xi` + 1 . From the truth table of f it is easy to see that K 0 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 0 . The negative case follows analogously. t u Example 2 illustrates the previous proposition. A lower number of clauses can also produce linear polynomials, but we have to allow clauses of different lengths. Proposition 6. (a) Let ϕ, ψ be propositional logic formulas. Then we have ϕ ≡ (ϕ ∨ ψ) ∧ (ϕ ∨ ψ̄) . (b) Let c, w be clauses. The set {c} is equivalent to {c ∪ w, c ∪ w̄}. (c) In the setting of (b), assume that w has length k . Write w = {L1 , . . . , Lk } with literals Li . Then the set {c} is equivalent to the set of all 2k clauses of shape c ∪ {L∗1 } ∪ · · · ∪ {L∗k } , where L∗i equals to Li or L̄i . Proof. Claim (a) can be easily proven by comparing a truth table for ϕ and (ϕ ∨ ψ) ∧ (ϕ ∨ ψ̄) . The other claims are immediate consequences of (a). t u The following example illustrates this proposition.  Example 7. Let B = {X1 , X2 }, {X̄1 , X2 , X3 }, {X1 , X̄2 , X3 }, {X̄1 , X̄2 , X̄3 } . The first clause in B is equivalent to the two clauses {X1 , X2 , X3 } , {X1 , X2 , X̄3 } . In view of this, we have covered all four possible combinations for negative signed clauses of length 3 . Indeed, Algorithm 3 converts B into x1 + x2 + x3 and x2 x3 + x2 + x3 + 1 . Proposition 6 leads to the following combinatorial test for checking whether a set of clauses B converts to a linear polynomial. 11 Proposition 7. Let B = {c1 , . . . , ck } be a set of clauses and V = {Xi1 , . . . , Xi` } be a set of ` variables in var(B) . For j = 1, . . . , k define the following sets: + Bj,V = {c ⊆ V ∪ V̄ | cj ⊆ c, #c = `, c has positive sign}, − Bj,V = {c ⊆ V ∪ V̄ | cj ⊆ c, #c = `, c has negative sign}. (1) If \  X + 2`−1 = (−1)#J−1 · # Bj,V , ∅6=J⊆{1,2,...,k} j∈J then the ideal generated by any algebraic representation of B contains xi1 + · · · + xi` + 1 . (2) If \  X − 2`−1 = (−1)#J−1 · # Bj,V , ∅6=J⊆{1,2,...,k} j∈J then the ideal generated by any algebraic representation of B contains xi1 + · · · + xi` . Proof. Let us focus on the first (i.e., positive) case. The second case is analogous. + In view of Proposition 6, the set Bj,V contains all possible extensions of cj in variables V to positive clauses of length `. We search for a complete signed + set in the union of all sets Bj,V . In other words, the cardinality of this union must be equal to 2`−1 in order to contain a complete signed set. Note that these sets may not Skbe disjoint. Thus we use the inclusion-exclusion principle for +  determining # j=1 Bj,V . t u In practice we do not have to apply the inclusion-exclusion principle, if the programming language we use has “set” as a built-in data structure. Algorithm 4 + − is a straight-forward application of Proposition 7. The sets Bj,V and Bj,V can be computed by extensions to the prescribed length ` via brute-force and grouping the result according to sign. Note that the ideas behind Algorithm 4 can be fur- ther developed, and a more efficient algorithm can be designed. (Some attempts in this direction can be deduced from the source code of CryptoMiniSat, see src/xorfinder.cpp in [19].) Since we have to check all subsets of var(B) in Step 2, Algorithm 4 is only practical for rather small-sized sets var(B) . Even if we are still able to directly derive linear polynomials from a large set of clauses C by Algorithm 4, the following proposition shows that Algorithm 3 produces at least the same number of linear polynomials. Proposition 8. Let C be a set of clauses, let I be the ideal generated by an algebraic representation of C , and let σ be a degree compatible term ordering. (1) Let L ⊂ I be an LTσ -interreduced set of linear polynomials. Let G be the reduced Boolean σ -Gröbner basis of I . Then we have #L ≤ #{g ∈ G | deg(g) = 1}. 12 Algorithm 4 (Combinatorial Search for Linear Polynomials) Input: A set of clauses B = {c1 , . . . , ck } . Output: A set of linear polynomials L such that the ideal generated by any algebraic representation of B contains L. 1: L0 := ∅ 2: foreach subset V = {Xi1 , . . . , Xi` } of var(B) do 3: B + := ∅ 4: B − := ∅ 5: for j = 1, . . . , k do + 6: B + := B + ∪ Bj,V − − − 7: B := B ∪ Bj,V 8: end for 9: if #B + = 2`−1 then 10: L0 := L0 ∪ {xi1 + · · · + xi` + 1} 11: end if 12: if #B − = 2`−1 then 13: L0 := L0 ∪ {xi1 + · · · + xi` } 14: end if 15: end foreach 16: Let L be an LTσ -interreduced F2 -basis of hL0 iF2 17: return L (2) Let m = 2 be an overlapping number. Let L be the output of Algorithm4( C ). Let S be the output of Algorithm3( C, σ, m). Then we have #L ≤ #{s ∈ S | deg(s) = 1} . Proof. (1) Let f ∈ I = hGi be a linear polynomial. If LTσ (f ) ∈ I , then LTσ (f ) ∈ G and we are done. In the other case, we know that LTσ (f ) is minimal in LTσ (I) with respect to divisibility. The tail of f can be reduced only by linear polynomials, and this results in a linear polynomial again. After all reductions we still have a linear polynomial in G. (2) Assume that Algorithm4( C ) has discovered a set of clauses K which con- tains 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) . t u During our experiments, we found that conversion of a Boolean system to CNF and back to ANF may give us enough linearly independent linear polynomi- als to solve the initial system S . Note that having n linearly independent linear polynomials in the ideal hSi ⊂ Bn 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. 13 Algorithm 5 (Generating Linear Polynomials in the Ideal) Input: A set of Boolean polynomials S , a degree compatible term ordering σ , and an overlapping number m ∈ N. Output: A set of linear polynomials in hSi . Requires: Algorithm 3 1: Compute a logical representation of S by a sparse conversion method. Call the result C . 2: Q := Algorithm3( C, σ, m ) 3: L := {l ∈ Q | deg(l) = 1} 4: return L 7 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 In- tel(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]. Instances of type AES-a -b- c- d represent propositional formulae in CNF derived from the gate level circuit implementation of the Small-scale AES with a rounds, the state matrix of size b × c and d -bit words in each state cell. Instances of type fact-a- b represent the problem of factoring the product a · b for the given two primes a, b. 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 Al- gorithms 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 Bc 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 Algo- rithm 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 con- versions of the block Bc 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 14 Instance CNF Algorithm 1 Algorithm 3 #vars #clauses #lin #quad #high #lin #quad #high AES-10-1-2-4 1081 3361 1 1792 1568 337 2194 0 AES-10-1-4-4 1862 5824 1 2986 2837 604 3692 0 AES-10-2-2-4 2441 7841 1 3584 4256 947 4407 0 AES-10-2-4-4 4289 13904 1 5986 7917 1785 7353 0 AES-10-4-1-4 3149 10065 1 4800 5264 1149 5915 0 AES-2-1-2-4 237 701 1 360 340 70 453 0 AES-2-1-4-4 412 1218 1 598 619 132 746 0 AES-2-2-2-4 526 1615 1 716 898 201 882 0 AES-2-2-4-4 935 2883 1 1196 1686 375 1491 0 AES-2-4-1-4 669 2065 1 960 1104 241 1191 0 AES-2-4-2-4 1157 3652 1 1434 2217 501 1778 0 AES-2-4-4-4 2077 6596 1 2394 4201 957 2978 0 fact-12601-18701 745 3853 2 616 3235 291 1365 2 fact-151-283 271 1333 2 250 1081 115 471 2 fact-1777-491 403 2029 2 354 1673 166 713 2 fact-2393-3371 466 2380 2 400 1978 181 855 2 fact-373-929 328 1640 2 294 1344 131 593 2 fact-583909-600203 1280 6784 2 1010 5772 471 2428 2 fact-59-1009 328 1640 2 294 1344 149 544 2 fact-59441-62201 826 4312 2 676 3634 318 1527 2 fact-81551-100057 947 4945 2 770 4173 359 1767 2 fact-9601-10067 638 3296 2 532 2762 243 1188 2 Table 1. (Number of converted polynomials by degree.) can be overcome by defining local Boolean rings for each Bc and then rewriting the local variables in Bc to their global names. Note that # var(Bc ) tends to be much smaller than # var(C) . Moreover, caching of the standard representations Ql of short clauses is possible. Polynomials of type i=1 (xi + ai ) can be precom- puted and stored in ANF for small values of `. Then the corresponding values ai ∈ F2 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. Acknowledgments. The authors thank Martin Albrecht and Alexander Dreyer for providing us with a better insight into the structure of Sage and PolyBoRi, as well as Mate Soos for helpful discussions about the implementation of SAT solvers. This work was financially supported by the DFG project “Algebraische Fehlerangriffe” [KR 1907/6-1]. 15 References 1. Audemard, G., and Simon, L. Glucose in the SAT 2014 Competition. In SAT Competition 2014: Solver and Benchmark Descriptions (2014), Univ. of Helsinki, pp. 31–32. 2. Bard, G. Algebraic Cryptanalysis. Springer, Heidelberg, 2009. 3. Bard, G. V., Courtois, N. T., and Jefferson, C. Efficient methods for con- version and solution of sparse systems of low-degree multivariate polynomials over GF(2) via SAT-solvers. IACR Cryptology ePrint Archive. 4. Bebel, J., and Yuen, H. Hard SAT instances based on factoring. In SAT Competition 2013: Solver and Benchmark Descriptions (2013), Univ. of Helsinki, p. 102. 5. Brickenstein, M. Boolean Gröbner Bases: Theory, Algorithms and Applications. Logos Verlag, Berlin, 2010. 6. Brickenstein, M., and Dreyer, A. PolyBoRi: a framework for Gröbner basis computations with Boolean polynomials. J. Symbolic Comput. 44 (2009), 1326– 1345. 7. Condrat, C., and Kalla, P. A Gröbner basis approach to CNF-formulae prepro- cessing. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2007), Springer, pp. 618–631. 8. Courtois, N. T., and Patarin, J. About the XL algorithm over GF(2). In Cryptographers Track at the RSA Conference (2003), Springer, pp. 141–157. 9. Courtois, N. T., Sepehrdad, P., Sušil, P., and Vaudenay, S. ElimLin algo- rithm revisited. In Fast Software Encryption (2012), Springer, pp. 306–325. 10. Dreyer, A., and Nguyen, T. H. Improving Gröbner-based clause learning for SAT solving industrial sized Boolean problems. In Young Researcher Symposium (YRS) (Kaiserslautern, 2013), Fraunhofer ITWM, pp. 72–77. 11. Een, N., and Sörensson, N. MiniSat: A SAT solver with conflict-clause mini- mization, 2005. see http://minisat.se. 12. Faugère, J.-C. FGb: a library for computing Gröbner bases. In International Congress on Mathematical Software (2010), Springer, pp. 84–87. 13. Gay, M., Burchard, J., Horáček, J., Messeng Ekossono, A. S., Schubert, T., Becker, B., Kreuzer, M., and Polian, I. Small scale AES toolbox: alge- braic and propositional formulas, circuit-implementations and fault equations. In Conf. on Trustworthy Manufacturing and Utilization of Secure Devices (TRUDE- VICE 2016) (Barcelona, 2016). 14. Horáček, J., Kreuzer, M., and Messeng Ekossono, A. S. Computing Boolean border bases. In 18th International Symposium on Symbolic and Nu- meric Algorithms for Scientific Computing, SYNASC (Timisoara, 2016), IEEE, pp. 465–472. 15. Hsiang, J. Refutational theorem proving using term-rewriting systems. Artif. Intell. 25 (1985), 255–300. 16. Jovanovic, P., and Kreuzer, M. Algebraic attacks using SAT-solvers. Groups Complex. Cryptol. 2 (2010), 247–259. 17. Kreuzer, M., and Robbiano, L. Computational Commutative Algebra 1. Springer, Heidelberg, 2000. 18. Schubert, T., and Reimer, S. antom, 2016. see https://projects.informatik. uni-freiburg.de/projects/antom. 19. Soos, M. CryptoMiniSat SAT solver v5.0.1, 2016. see http://www.msoos.org. 16 20. The ApCoCoA Team. ApCoCoA: Applied Computations in Commutative Alge- bra. available at http://apcocoa.uni-passau.de. 21. The Sage Developers. SageMath, the Sage Mathematics Software System (Ver- sion 7.5.1), 2017. see http://www.sagemath.org. 22. Zengler, C., and Küchlin, W. Extending clause learning of SAT solvers with Boolean Gröbner bases. In International Workshop on Computer Algebra in Sci- entific Computing (2010), Springer, pp. 293–302. 17