On Conversions from CNF to ANF

Abstract

In this paper we discuss conversion methods from the conjunctive normal form (CNF) to the algebraic normal form (ANF) of a Boolean function. Whereas the reverse conversion has been studied before, 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 blockwise 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 nds 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 polynomial
• Boolean Grobner basis
• SAT solving

-

The Boolean satis ability problem (SAT) and polynomial system solving over a nite eld (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 nite eld, 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 nd one or all satisfying assignments, or to nd one or all common zeros.

E cient 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 e cient 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 Grobner basis techniques into the various stages of a SAT solver.

Our motivation for studying more e cient 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 Grobner 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 de nitions 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 brie y 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 e cient 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 Grobner basis. As it turns out, the Grobner 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 Grobner bases encompasses algebraic versions of the usual DPLL rules of inference (cf. Prop. 4).

The task of nding 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 su ciently 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 Grobner 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 su cient to solve the Boolean polynomial system, because the blockwise conversion algorithm produces enough linear polynomials to allow Gau ian elimination to work.

The nal 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 de nitions and notation of [ 17 ]. 2

Background

In this section we recall basic de nitions and known results and introduce useful notation. In the following we let F2 be the eld of two elements and F2[x1; : : : ; xn] a polynomial ring over F2 . The ideal F = hx12+x1; : : : ; x2n+xni is called the eld ideal, since it is the vanishing ideal of F2n . 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 algebraic normal form (ANF). An arbitrary polynomial f can be transformed to ANF by computing its normal form NFF (f ) with respect to the eld ideal. Notice that we use \ + " instead of \ " for addition in F2 .

Given a set S = ff1; : : : ; fsg Bn , we de ne the set of F2 -rational zeros of S by

n

Z(S) = fa 2 F2 j f (a) = 0 for all f 2 Sg: In fact, the set Z(S) does not depend on the particular choice of generators of the ideal I = hf1; : : : ; fsi , 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 Grobner 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) Grobner Basis Algorithm, the library PolyBoRi [ 6 ] and the FGb library [ 12 ] provide e cient 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 Grobner bases, we refer to [5, Ch. 2]. Every ideal I Bn can be represented by an ideal I0 F2[x1; : : : ; xn] such that F I0 . Hence Boolean Grobner bases correspond to Grobner bases of ideals containing the eld 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 Xi . A set of clauses C = fL1;1; : : : ; L1;n1 g; : : : ; fLk;1; : : : ; Lk;nk g 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 .

Next we de ne the set of satisfying assignments for a given set of clauses C in n logical variables by

SAT(C) =

a 2 fFalse; Truegn j C(a) evaluates to True : The algorithms that search for a satisfying assignment for C are called SAT solvers. In order to nd 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 con ict 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 . De nition 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 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 n represents the unique Boolean function F2 ! F2 mapping a 7! 0 if a 2 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 e cient 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 rst 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. For each assignment that yields True , we construct one clause that eliminates this particular assignment. Thus the set of clauses C = fX1; X2g; fX1; X2g; fX1; X2g is the logical representation of the polynomial f . Note that the set fx1; x2 + 1g 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 2 Bn 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 x1x2x3 by encoding t + x1x2x3 to the clauses fX1; T g , fX2; T g , fX3; T g , fX1; X2; X3; T g . 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 prede ned 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 fX1; X2; X3; X4g; fX1; X2; X3; X4g; fX1; X2; X3; X4g; fX1; X2; X3; X4g; fX1; X2; X3; X4g; fX1; X2; X3; X4g; fX1; X2; X3; X4g; fX1; X2; X3; X4g: Both conversions su er 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 = fL1; L2; : : : ; Lmg be a clause of C . The assignment (a1; : : : ; an) 2 F2n satis es 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 = Xi . tu 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 X1; : : : ; Xn .

Output: A set S Bn such that S is an algebraic representation of C . Example 3. Given the set of clauses ffX1; X2g; fX1; X2; X3g; fX4; X5g; fX1; X2; X3g; fX1; X2; X3g; fX4; X5g , the Standard CNF to ANF Conversion yields the following results:

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 S^ . Even if the computation of a Grobner basis of the ideal ^ hSi may be done in seconds, a Grobner basis of the ideal hSi 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 de nitions. De nition 2. (a) The set of variables Xi such that Xi or Xi 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 2 C has positive (resp. negative ) sign if the number of negative literals is an even (resp. odd) number. (c) We de ne the length of a clause c 2 C as the cardinality #c . (d) Let c; c0 2 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 2 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 2 N .

Output: A set of subsets B of C and a subset T of C such that for B 2 B with #B 2 and for every b 2 B , there exists an element b0 2 B n fbg with the property that m is an overlapping number for b and b0 , and such that SB2B B [ T = C and every clause in T contains less than m literals. 1: foreach c in C do 2: Bc := c0 2 C j # var(c) \ var(c0) m 3: end foreach 4: B0 := fBc j c 2 C; Bc 6= ;g 5: Let B be the set of maximal elements of B0 w.r.t. inclusion. 6: T := C n Sc2C 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 2 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 #2C intersections in Step 2, and at most #2B 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 2 N , we de ne an undirected graph Gm;C which has C as vertices and for which two distinct clauses c; c0 2 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 Algorithm 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.

tu

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 = fc1; c2; c3g with c1 = fX1; X2; X3; X4g , c2 = fX1; X2g and c3 = fX3; X4g , 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.

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 (g0) for all g; g0 2 G with g 6= g0 . Given an arbitrary set of Boolean polynomials G Bn , we can LT -interreduce G via Gau ian elimination on the coe cient 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 2 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 Grobner basis algorithm. 1: S0 := ; 2: Using Algorithm2( C , m ), compute a pair (B; T ) . 3: B := B [ St2T ftg 4: foreach B in B do 5: Q := Algorithm1( B ) 6: Let G be the reduced Boolean -Grobner basis of the ideal hQi , i.e., the reduced

Boolean Grobner basis with respect to the term ordering . 7: S0 := S0 [ G 8: end foreach 9: Let S ;m be an LT -interreduced F2 -basis of hS0iF2 such that its coe cient matrix w.r.t. is in reduced row echelon form. 10: return S ;m

It is di cult to give a meaningful upper bound for the time complexity of this algorithm, since it involves a number of Grobner 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 De nition 3), the conversion will contain a linear polynomial. In this case, the corresponding Grobner 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 Grobner 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 we prove that S ;m is an algebraic representation of C . In Step 3 we have SB2B Sc2B c = C , because every c 2 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 2 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 S0 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 -Grobner basis of the ideal hQi in Step 6 is unique, and so is the basis in Step 9. tu Example 6. Let us apply Algorithm 3 in the setting of Example 3. 2 fX1; X2g ! x1x2 + x1 + x2 + 1 3 6 fX1; X2; X3g ! x1x2x3 + x1x2 + x1x3 + x1 7 4 fX1; X2; X3g ! x1x2x3 + x1x2 + x2x3 + x1 75 6 fX1; X2; X3g ! x1x2x3 fX4; X5g ! x4x5 + x4 + x5 + 1 fX4; X5g ! x4x5 + x5 ! ! x2x3 + x2 + x3 + 1 x1 + x2 + x3 x4 + 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 Grobner basis algorithm can be interpreted as performing simple logical reasoning.

Proposition 4. In the setting of Algorithm 3, let B = fc1; : : : ; ckg be a set of clauses. Let Q = fq1; : : : ; qkg 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 -Grobner basis of the ideal I = hQi . (1) Let ci; cj 2 B be clauses such that ci is a proper subclause of cj . Then G is equal to the reduced Boolean -Grobner basis of hQ n fqj gi . (2) Let L be a literal and assume that cj = fLg is an element of B . Let fqi1 ; : : : ; qis g be the set of all clauses in B di erent from qj and containing the literal L . Then G is the reduced Boolean -Grobner basis of hQ n fqi1 ; : : : ; qis gi . (3) Let ci 2 B be of the form ci = c0 [ fXj ; Xj g for some clause c0 and a logical variable Xj . Then G is the reduced Boolean -Grobner basis of hQ n fqigi . (4) Assume that ci; cj 2 B satisfy ci = w [ fXeg and cj = w0 [ fXeg 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 = f1g: (6) Let #B 2 . If there exists a clause cj 2 B such that var(c0) var(cj ) holds for all c0 2 B , then we have maxfdeg(g) j g 2 Gg < maxfdeg(q) j q 2 Qg . (7) Let f 2 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 2 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 fqi1 ; : : : ; qis g 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 satis es qi = (xj2 + xj )f = 0 in Bn and the claim follows. (4) The standard algebraic representation of ci resp. cj is qi = xef resp. qj = (xe + 1)g for some polynomials f; g . The S-polynomial of qi; qj is equal to f g = g(xef ) + 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 eld 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 2 B such that ci cj and we apply Claim (1). If there is another q 2 Q with the maximal degree in Q di erent from qj , then LT (q) = LT (qj ) .

Hence we drop the degree at least by one after the LT-reduction. (7) We have f = Qj`=1(xij + aj ) for some aj 2 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 -Grobner basis of the ideal I . The claim follows form the uniqueness of the reduced Boolean -Grobner basis. tu

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 problem of identifying sets of clauses containing a linear polynomial in their algebraic representation.

De nition 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 de nition 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) = fXi1 ; : : : ; Xi` g . Then xi1 + + xi` + 1 (resp. xi1 + + xi` ) is the standard algebraic representation of K .

Proof. Let K0 be the sparse conversion of f = xi1 + + xi` + 1 . From the truth table of f it is easy to see that K0 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 = K0 . The negative case follows analogously. tu

Example 2 illustrates the previous proposition. A lower number of clauses can also produce linear polynomials, but we have to allow clauses of di erent lengths.

Proposition 6. (a) Let '; be propositional logic formulas. Then we have ' (' _ ) ^ (' _ ) . (b) Let c; w be clauses. The set fcg is equivalent to fc [ w; c [ wg . (c) In the setting of (b), assume that w has length k . Write w = fL1; : : : ; Lkg with literals Li . Then the set fcg is equivalent to the set of all 2k clauses of shape c [ fL1g [ [ fLkg , where Li equals to Li or Li .

Proof. Claim (a) can be easily proven by comparing a truth table for ' and (' _ ) ^ (' _ ) . The other claims are immediate consequences of (a). tu

The following example illustrates this proposition.

Example 7. Let B = fX1; X2g; fX1; X2; X3g; fX1; X2; X3g; fX1; X2; X3g . The rst clause in B is equivalent to the two clauses fX1; X2; X3g , fX1; X2; X3g . 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 x2x3 + x2 + x3 + 1 .

Proposition 6 leads to the following combinatorial test for checking whether a set of clauses B converts to a linear polynomial. Proposition 7. Let B = fc1; : : : ; ckg be a set of clauses and V = fXi1 ; : : : ; Xi` g be a set of ` variables in var(B) . For j = 1; : : : ; k de ne the following sets: Bj+;V = fc Bj;V = fc

V [ V j cj V [ V j cj c; #c = `; c has positive signg; c; #c = `; c has negative signg: (1) If (2) If + xi` + 1 .

+ xi` . then the ideal generated by any algebraic representation of B contains xi1 + 2` 1 =

X ;6=J f1;2;:::;kg ( 1)#J 1

# 2` 1 =

X ;6=J f1;2;:::;kg ( 1)#J 1 # \ Bj+;V ; j2J \ Bj;V ; j2J then the ideal generated by any algebraic representation of B contains xi1 + Proof. Let us focus on the rst (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 be disjoint. Thus we use the inclusion-exclusion principle for determining # Sjk=1 Bj+;V . tu

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 further developed, and a more e cient 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 -Grobner basis of I . Then we have #L #fg 2 G j deg(g) = 1g . Algorithm 4 (Combinatorial Search for Linear Polynomials) Input: A set of clauses B = fc1; : : : ; ckg .

Output: A set of linear polynomials L such that the ideal generated by any algebraic representation of B contains 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 #fs 2 S j deg(s) = 1g .

Proof. (1) Let f 2 I = hGi be a linear polynomial. If LT (f ) 2 I , then LT (f ) 2 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 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 2 B , and we can use (1) . tu

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 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. 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 2 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 := fl 2 Q j deg(l) = 1g 4: return L 7

Experiments

In this section we examine the e ciency 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 Grobner basis computations. We choose the speci c 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 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 Bc in Algorithm 2 that are too hard for the Grobner 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 Grobner bases of the conversions 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 Instance can be overcome by de ning 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 of short clauses is possible. Polynomials of type Qli=1(xi + ai) can be precomputed and stored in ANF for small values of ` . Then the corresponding values ai 2 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., con ict 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 nancially supported by the DFG project \Algebraische Fehlerangri e" [KR 1907/6-1].

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. E cient methods for conversion 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 Grobner Bases: Theory, Algorithms and Applications . Logos Verlag, Berlin, 2010 .

6. Brickenstein , M. , and Dreyer , A. PolyBoRi: a framework for Grobner basis computations with Boolean polynomials . J. Symbolic Comput . 44 ( 2009 ), 1326 { 1345 .

7. Condrat , C. , and Kalla , P. A Grobner basis approach to CNF-formulae preprocessing . 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. , Susil , P. , and Vaudenay , S. ElimLin algorithm revisited . In Fast Software Encryption ( 2012 ), Springer, pp. 306 { 325 .

10. Dreyer , A. , and Nguyen , T. H. Improving Grobner-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 Sorensson, N. MiniSat: A SAT solver with con ict-clause minimization , 2005 . see http://minisat.se.

12. Faugere , J.-C. FGb: a library for computing Grobner bases . In International Congress on Mathematical Software ( 2010 ), Springer, pp. 84 { 87 .

13. Gay , M. , Burchard , J. , Horacek , J. , Messeng Ekossono , A. S. , Schubert , T. , Becker , B. , Kreuzer , M. , and Polian , I. Small scale AES toolbox: algebraic and propositional formulas, circuit-implementations and fault equations . In Conf. on Trustworthy Manufacturing and Utilization of Secure Devices (TRUDEVICE 2016 ) (Barcelona , 2016 ).

14. Horacek , J. , Kreuzer , M. , and Messeng Ekossono , A. S. Computing Boolean border bases . In 18th International Symposium on Symbolic and Numeric Algorithms for Scienti c 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.

20. The ApCoCoA Team . ApCoCoA: Applied Computations in Commutative Algebra. available at http://apcocoa.uni-passau.de.

21. The Sage Developers . SageMath, the Sage Mathematics Software System (Version 7.5.1) , 2017 . see http://www.sagemath.org.

22. Zengler , C. , and Kuchlin, W. Extending clause learning of SAT solvers with Boolean Grobner bases . In International Workshop on Computer Algebra in Scienti c Computing ( 2010 ), Springer, pp. 293 { 302 .