In this paper we consider formulas that are conjunctions of linear clauses, i.e., of linear equations. Such formulas are very interesting because they encode CNF constraints that are typically very hard for SAT solvers. We introduce a new proof system SRES that works with linear clauses and show that SRES is implicationally and refutationally complete. Algebraically speaking, linear clauses correspond to products of linear polynomials over a ring of Boolean polynomials. That is why SRES can certify if a product of linear polynomials lies in the ideal generated by some other such products, i.e., the SRES calculus decides the ideal membership problem. Furthermore, an algorithm for certifying inconsistent systems of the above shape is described. We also establish the connection with an another combined proof system R(lin).
In this paper we deal with a special case of the ideal membership problem: given a set of Boolean polynomials S which are products of linear polynomials and a Boolean polynomial f which is also a product of linear polynomials, decide whether f ∈ S . Traditionally, one can use Gröbner bases to solve this problem. The assumption that the given polynomials are products of linear polynomials allows us introduce a new calculus, called SRES, that is tailored to tackle this problem. It needs only a lightweight version of the S -polynomials used Gröbner basis algorithms, namely the s-resolvents we introduced in [6]. These s-resolvents also generalize the classical resolution rule from propositional logic. Nevertheless, we consider SRES to be an algebraic proof system (in the sense of [5], [2] or [4]), and hence we mostly use the terminology of commutative algebra to describe it. The main difference in the algebraic approach is that we study assignments that yield False, i.e., are zeros of a system, in constrast to look for assignments that yield True in the SAT terminology.
From the propositional logic point of view, we would like to decide if the semantic implication S |= f holds. Recall that a linear Boolean polynomial x i1 + • • • + x ij corresponds to a linear XOR constraint x i1 ⊕ • • • ⊕ x ij . Such constraints are very difficult for SAT solvers because the truth value depends genuinely on all variables, i.e., changing the value of one variable results in flipping the truth value of the XOR. Many hard formulas in CNF can be constructed by combining literals into linear XOR constraints, resulting in so-called linear clauses. For details, we refer the readers to [1] or [12]. Such formulas appear quite frequently in cryptography, where linear constraints are typically mixed with highly nonlinear ones, for instance in substitution permutation networks. Another application is to handle the bit-blasted version of ARX operations (Add-Roll-Xor) which is becoming a popular part of ARX ciphers. When converted to bit-wise operations, these conversions give XOR-heavy formulae with a handful of AND gates describing the carry chains of the adders.
The paper is organized as follows. In Section 2 we recall the definition of linear clauses and introduce several ways of describing them, in particular using products of linear Boolean polynomials. Our main data structure to describe them is the set of linear polynomials that appear in the linear clause.
In Section 3 we define the proof system SRES which incorporates and extends the s-resoution rule defined in [6]. We prove that the SRES proof system is implicationally and refutationally complete. Moreover, we establish a relation with other combined systems that use resolution and polynomial calculus (see [11]). In particular, we show that SRES simulates the proof system R(lin) defined in [7,11].
In Section 4 we describe a concrete algorithm that searches for SRES-refutation proofs of inconsistent systems, called the SRES Refutation Algorithm, and compare it to other approaches to the problem at hand. Finally, in Section 5, we apply the SRES Refutation Algorithm to some examples and point out possible further improvements.
In the following we use some of the definitions and results given in [6], in particular the algorithm Sres given there. However, to aid the readers, we tried to make the paper as self-contained as possible and mention any overlaps explicitly.
Let F 2 = Z/2Z be the binary field and F 2 [x 1 , . . . , x n ] a polynomial ring over F 2 . The ring
x n is called the ring of Boolean polynomials in the indeterminates x 1 , . . . , x n . Let L n be the set of all linear polynomials in F 2 [x 1 , . . . , x n ] , i.e., the set of all polynomials of degree ≤ 1 . (Here we use deg(0) = −1 .)
Throughout the paper we consider the obvious correspondences between the following types of objects, where 1 , . . . , k ∈ L n :
Next we give an example of the above correspondence.
To simplify the notation, we view the sets in (C1) as polynomials in (C2), e.g., we speak of zeros of H instead of zeros of h. Furthermore, we always assume that the linear polynomials 1 , . . . , k appearing in (C1) are pairwise distinct, i.e., that the set H does not contain duplicates. The notion of linear clauses has been considered before in [7,11]. Note that many difficult CNF instances can be naturally encoded in the form (C3). Thus we are targeting very hard formulas (see [10,Sec. 3]). Furthermore, we observe that two different subsets in (C1) may represent the same polynomial, as the following example shows.
Example 2 Consider the sets of linear polynomials {x 3 , x 2 + x 3 , x 1 + x 3 + 1} and {x 3 , x 1 +x 2 , x 1 +x 3 +1} as in (C1). Then we have x 3 (x 2 +x 3 )(x 1 +x 3 +1) = x 3 (x 1 + x 2 )(x 1 + x 3 + 1) in B 3 , i.e. the corresponding polynomials in (C2) agree.
The subsets in (C1) are measured by degree and size. We recall here some definitions from [6] and [11].
(1) The number deg(h) = #H is called the degree of H .
(2) For ∈ L n , we let var( ) be the set of indeterminates occurring in . We call the number size(H) = # var( 1 ) + • • • + # var( k ) the size of H .
Our goal in this paper is to show that a given set of linear clauses is unsatisfiable. For this purpose, we define semantic implication as follows.
Definition 4 Let F 1 , . . . , F m , H ⊆ L n . We say that F 1 , . . . , F m semantically imply H if every F 2 -rational common zero of the Boolean polynomials corresponding to F 1 , . . . , F m is a zero of H . In this case we write F 1 , . . . , F m |= H .
From the algebraic point of view, we have F 1 , . . . , F m |= H if and only if H ∈ F 1 , . . . , F m ⊆ B n . Note that the zeros of an ideal in B n are always F 2rational, because ideals in B n correspond to ideals in F 2 [x 1 , . . . , x n ] that contain the field ideal x 2 1 + x 1 , . . . , x 2 n + x n . Using the newly defined terminology, we can say that our goal is to refute a given set of linear clauses, i.e. to prove that the corresponding sets of linear polynomials semantically imply {1} .
Recall that a proof system, sometimes called a Hilbert system or Hilbert calculus, consists of a syntax, i.e. a set of rules which determine the set of well-formed formulas of the system, by a set of axioms, i.e. a set of formulas which are assumed to be tautologies, and by its set of rules of inference, i.e. by a set of rules which determine how one can get new tautologies from known ones.
For instance, the Gröbner proof system defined in [5] admits all formulas of the form f (x 1 , . . . , x n ) = 0 where f ∈ F 2 [x 1 , . . . , x n ] . Its axioms are the Boolean axioms x 2 i + x i = 0 for i = 1, . . . , n , and its rules of inference are f g f + g (P a ) and
where f, g ∈ F 2 [x 1 , . . . , x n ] and x i is an indeterminate.
In this section we continue to study the proof system based on s-resolution which was introduced in [6]. More precisely, we extend that system by other inference rules, and thus we define the new proof system called SRES. Let us begin by recalling the proof system in [6].
Definition 5 The proof system s-resolve is defined by the following parts:
(1) A formula is a set of linear polynomials { 1 , . . . , s } ⊂ L n , where s ∈ N + .
(2) The axioms are the Boolean axioms given by {x i , x i + 1} for i = 1, . . . , n .
(3) There exists one rule of inference (R) , namely
where G, G ⊆ L n and s ≥ 1 . This rule is also called s-resolution. (For s = 1 , we let
The result of an application of the s-resolution rule is called an s-resolvent.
Let us note that the Boolean axioms immediately imply the following remark.
Remark 6 By applying 2-resolution to the axioms {x i , x i +1} and {x i +1, x i } , we obtain that {0} is a tautology in the s-resolve proof system.
In [6] we showed that s -resolve is correct in the sense of the following definition.
Definition 7 Let (I) be a rule of inference of a proof system. We say that the rule of inference (I) is correct if
For s ≥ 3 , the s -resolution rule depends e.g. on the numbering of the linear polynomials. (2-resolvents are unique because there is only one way how to form the linear polynomial 1 + 2 +1 .) However, considered as a Boolean polynomial, the s-resolvent is uniquely determined. The next example is a point in case. Definition 9 The proof system SRES is defined by the following parts.
(1) The syntax agrees with the syntax of s -resolve, i.e. a formula is a set of linear polynomials { 1 , . . . , s } ⊂ L n , where s ∈ N + . (2) The axioms are the Boolean axioms {x i , x i + 1} for i = 1, . . . , n .
(3) The rules of inference consist of s-resolution (R) and the following weakening rule (W) :
Since we trivially have H |= H ∪ { } , the proof system SRES is correct with respect to semantic implication. Next we recall the definition of a proof.
Definition 10 Let PS be a proof system. A PS-proof of a formula H from the initial premises F 1 , . . . , F m in the proof system PS is a sequence of formulas π = (G 1 , . . . , G k ) such that G k = H and each of the formulas G i is of one of the following forms:
(1) G i ∈ {F 1 , . . . , F m } (2) G i is one of the axioms of PS.
(3) G i is obtained from some of the formulas G j with j < i by applying one of the rules of inference of the proof system PS.
If a formula H has a PS-proof from {F 1 , . . . , F m } , we write F 1 , . . . , F m PS H , or simply F 1 , . . . , F m H if no confusion can arise. Since the proof system SRES is correct, our goal to refute {F 1 , . . . , F m } can now be expressed by asking that we should prove F 1 , . . . , F m {1}. Notice that the intended semantics is that an unsatisfiable formula corresponds to polynomial equations i,1 • • • i,s = 0 for i ∈ {1, . . . , m} which has no solution. Equivalently, a tautology is an equation which holds for all points of F n 2 . A proof can be seen as a sequence of applications of rules to axioms or previously proved tautologies.
Next we extend the capabilities of our proof system by deriving the following further rules of inference.
Definition 11 Let F, G be subsets of L n , and let , 1 , 2 ∈ L n .
(1) The rule (U) defined by
is called unit cancellation.
(2) The rule (MP) defined by
is called modus ponens.
(3) The rule (A) defined by
is called the addition rule.
Proposition 12 The rules (U) , (MP) , and (A) are correct. Furthermore, any proof derived using (U), (MP) and (A) can be rewritten into an SRES-proof.
Proof. The correctness of (U) follows from the observation that multiplying a Boolean polynomial by 1 does not change its zeros. Using Remark 6 we apply 1 -resolution on H ∪ {1} and {0}, and we get H . To prove modus ponens it suffices to use (R) with s = 1 and G = ∅. Finally, we show the correctness of (A) . Using the weakening rule, we infer F ∪ { 1 , 2 + 1} from F ∪ { 1 } and H ∪{ 2 , 1 +1} from H ∪{ 2 } . Then, using 2 -resolution, we get F ∪H ∪{ 1 + 2 } .
The following remark and the subsequent proposition will become important later in the proof of Proposition 18.
Remark 13 Let π = (H 1 , . . . , H k ) be an SRES-proof of H k from F 1 , . . . , F m that uses only the s-resolution rule. Let be an element of one of the sets H i . Then lies in the F 2 -vector space generated by the linear polynomials contained in the union m i=1 F i .
Proposition 14 Let F ⊆ L n and let i ∈ {1, . . . , n}. For a ∈ {0, 1} , let F (x i → a) denote the set which is obtained by substituting x i → a into the linear polynomials contained in F . Then the following claims hold true for i ∈ {1, . . . , n}.
Proof. First we prove (1). Let ∈ F be such that x i occurs in . The polynomial x i + corresponds to substituting x i = 0 into . This addition can be derived in SRES using Proposition 12. The claims (2)-( 4) follow analogously from Proposition 12.
The next example illustrates this proposition.
Example 15 Let F 1 = {x 1 + x 2 , x 1 } and F 2 = {x 1 + 1} . By Proposition 12, there exists an SRES-proof of the set {x 2 + 1, 1} from F 1 , F 2 which corresponds to the substitution of x 1 = 1 into F 1 . On the other hand, we can "backtrack" the substitution, i.e. we have
The following example shows an important advantage of the SRES proof system over the Gröbner proof system defined in [5]. More precisely, it shows that the data structures (C1)-(C3) efficiently store dense linear clauses.
Example 16 Consider the sets
On one hand, it is easy to see that the system is inconsistent because substituting F 2 , . . . , F n+1 into F 1 gives us 1 . On the other hand, the input for the Gröbner basis algorithm is assumed to be expanded (i.e., not in the form of products of linear polynomials). We can always find n ∈ N such that expanding F 1 to the polynom f 1 = n i=1 (x i + x i+1 ) , which has 2 n terms, exceeds the available memory, and hence any Gröbner basis algorithm can not be applied. Notice that we have size(F 1 ) = 2n .
One workaround would be to introduce new indeterminates to break the long product, but it does not help too much because the Gröbner basis algorithm substitutes the new indeterminates back, and thus recovers the expanded polynomial F 1 again.
However, by Proposition 14, there exists a short SRES refutation that corresponds to the substitution of F 2 , . . . , F n+1 into F 1 .
The following definition provides further useful properties of proof systems.
Definition 17 (1) A proof system is called implicationally complete if for every formula H and every set of formulas {F 1 , . . . , F m } such that we have F 1 , . . . , F m |= H , there exists a proof of H from F 1 , . . . , F m in this proof system. (2) A proof system is called refutationally complete if for every inconsistent set of formulas {F 1 , . . . , F m } , i.e. for F 1 , . . . , F m |= {1}, there exists a proof of {1} from F 1 , . . . , F m in this proof system.
The proof of the following proposition is inspired by the corresponding proof for the classical resolution calculus (see for instance [3,Th. 4.1.5]) and by the proof given in [11, Th. 5.1]) Proposition 18 The proof system SRES is implicationally and refutationally complete.
Proof. First we show that SRES is implicationally complete. Let F 1 , . . . , F m , H ⊆ L n be sets of linear polynomials such that F 1 , . . . , F m |= H . We want to prove that F 1 , . . . , F m SRES H . We proceed by induction on the number
Let us consider the case k = 0 , i.e. the case when all linear polynomials in F i and H are constants 0 or 1. If all sets F 1 , . . . , F m are equal to {0}, there is trivially an SRES-proof of {0}. All the semantic implicants of {0} of size 0 can be derived from {0} by the weakening rule. If there exists a set F i = {1} , then there is trivially an SRES-proof that refutes F 1 , . . . , F m , and hence we can derive any linear clause by the weakening rule and the unit cancellation rule. Finally, if F i = {0, 1}, then F i is simplified to {0} by unit cancellation, and thus we can use the previous argument. Now assume that the claim holds for some k ≥ 0 and consider a semantic implication
denote the set which is obtained by substituting x i → a into the linear polynomials contained in F . By Proposition 14, we have F j , {x i } SRES F j (x i → 0) for j = 1, . . . , m . Moreover, we clearly have F 1 (x i → 0), . . . , F m (x i → 0) |= H(x i → 0) . By the induction hypothesis, there is an SRES-proof of H(x i → 0) from F 1 (x i → 0), . . . , F m (x i → 0) . Altogether, we get
Furthermore, by Proposition 14, we have H(x i → 0), {x i } SRES H . All in all, there is an SRES-proof π 1 of H from {x i }, F 1 , . . . , F m . Analogously, we get an SRES-proof π 2 of H from {x i + 1}, F 1 , . . . , F m .
Next we modify the derivations of π 1 (resp. π 2 ) such that they start from
Note that the same rules of inference can be applied, and thus one can rewrite the proof π 1 into an SRES-proof α 1 from {x i , x i + 1}, F 1 , . . . , F m of either H or H ∪ {x i }. Similarly, we rewrite π 2 into an SRES-proof α 2 from {x i , x i + 1}, F 1 , . . . , F m of H or H ∪ {x i + 1}. If the proof α 1 or α 2 ends with H , we are done. Otherwise, we have H ∪ {x i }, H ∪ {x i + 1} SRES H by a single step of the 1 -resolution rule, which concludes the proof. The SRES proof system is in fact a combined proof system in the sense of [8,Sec.7.1]. For instance, R(lin) in [11] is an another example of a combined proof systems that combines resolution with polynomial calculus. By Proposition 12 we immediately get that SRES efficiently simulates the system R(lin). This means that there exists a polynomial-time algorithm that translates any R(lin)-proof of H from F 1 , . . . , F m to an SRES-proof of H from F 1 , . . . , F m .
On the other hand, SRES cannot simulate the rule (P a ) of the Gröbner proof system because addition of two products of linear polynomials does not have to be a product of linear polynomials in B n , e.g., x 1 • x 2 + 1 cannot be written as a product of linear polynomials in B 3 .
In [6] the authors introduced an algorithm that finds refutation proofs for unsatisfiable formulas in CNF using s-resolution. In this section we generalize this result to formulas that are conjuctions of linear clauses and show that it is refutationally complete in the sense of Definition 17. We recall the following algorithm for computing the s-resolvent of two polynomials which is described in [6].
return {1} 7: else 8:
for i = 1, . . . , s − 1 do 9:
return {0} 13:
end if 14:
end for 15: end if 16: return R Algorithm 2 extends two polynomials by the weakening rule in all possible ways such that s-resolution can be applied. More precisely, this set of extensions is defined as follows.
Definition 19 Let F, G ⊆ L n . The set of all pairs K ⊆ L n × L n such that the following two conditions hold for all (F , G
Condition (1) encodes the fact that there exists at least one ∈ L n in F and G on which we can s-resolve. Condition (2) restrains F , G to contain linear polynomials or + 1 such that ∈ F ∪ G. Note that the set of expansions for F, G is unique.
Algorithm 2 produces the set of expansions in a brute-force way, i.e., Condition ( 1) is implemented in Step 10, and Condition ( 2) is fulfilled because of the two foreach loops in Steps 3, 4.
Algorithm 2 AllExpansions (All Possible Expansions to s-Resolution)
Output: The set of expansions for F, G .
Write A = (a1, . . . , a k ) . 6:
Write B = (b1, . . . , b k ) . 7:
Minimize the representation of F and G by applying unit cancellation, i.e., remove the element 1 from F , G . 10:
end if 13:
end foreach 14: end foreach 15: return K
The next example shows the generation of the pairs in Algorithm 2.
Next we process the pairs computed by Algorithm 2 in increasing order with respect to the following ordering relation.
and size(F ) < size(G) .
(
Note that the size of the s-resultants can be determined without actually executing Sres (see [6,Alg. 8]). Now we are ready to present Algorithm 3 for constructing SRES-refutations. We assume that all sets occurring in the algorithm do not contain duplicates, i.e., that removal of duplicates is applied whenever possible. This is the classical assumption on sets in programming languages such as python. Proof. Finiteness follows from the fact that there are only finitely many linear polynomials in L n . Hence the sets in S are finite, and so is the set P ⊆ L n ×L n .
The algorithm is correct because the SRES inference rules semantically imply their results.
It remains to show that the algorithm is refutationally complete. Assume that the ideal generated by the polynomials corresponding to the input sets has no common zero. By Proposition 18, we know that there exists an SRES-refutation of F 1 , . . . , F m . The Boolean axiom is incorporated in Step 6, and weakening takes place in the function AllExpansions such that all possible choices to form an s -resolvent are created for all possible s ∈ N + . The s-resolution rule is then applied by calling Sres. Any set Q that is a proper superset of some set already occurring in S is ignored because all possible s -resolvents that would be created using Q are at that time already in P . Thus the algorithm sequentially creates all SRES-derivations from F 1 , . . . , F m . It arranges the computation such that "smaller" sets in terms of size are preferred. Since Proposition 18 shows that there exists an SRES-refutation, the set {1} is eventually discovered by the algorithm.
The list P in Algorithm 3 can be implemented as a min-heap such that the minimal pair is always easily found and extracted. The number of pairs in P may be huge. Thus it is convenient to compute the s -resolvents only in Step 10. The next example indicates how the pairs can be stored. The s-resolvent is created only if its size is minimal.
can be stored as a tuple (1, {x 2 }, 2, ∅, 1) with the meaning "Sres of F 1 ∪ {x 2 } and F 2 ∪ ∅ has size 1".
Recall that we need to know the sizes of all s-resultants in P in order to select the minimum. Thus the chosen format is very convenient because the size of the s -resolvent can be predicted as in [6,Alg. 8] without computing the actual s-resolvents.
Furthermore, one can form only 2-resolvents in Algorithm 3 since 2-resolution is enough to simulate R(lin) which is implicationally and refutationally complete. However, "extra" linear clauses coming from s-resolution steps with s ≥ 3 may come in handy, and the refutation can be found faster in Algorithm 3.
In this section we give some examples of the SRES proof system. Initial experiments on refuting CNF formulae using SRES can be found in [6,Sec. 9]. Those experiments were focused on comparing resolution with SRES based on CNF benchmarks coming from [10]. These formulae are hard for classical resolution, but there may exist short refutations in other axiomatic systems of propositional calculus [13].
In the following example taken from [5], we compare SRES with algebraic systems such as the Gröbner proof system and the Nullstellensatz system [4, Def. Example 24 Consider the polynomials
. They encode two implications x 1 → x 2 and x 2 → x 3 . (E.g., if
x 1 = 1 , then x 2 is constrained to be 1.) Let us write a proof of h = x 1 + x 1 x 3 , i.e., the implication x 1 → x 3 , in the Gröbner proof system. Firstly, we multiply f 2 by x 1 , and we get
Note that the maximal degree appearing in the proof is 3 . On the other hand, there exists a Nullstellensatz proof of the maximal degree O(log(n)) of x 1 → x n from x 1 → x 2 , . . . , x n−1 → x n (see [5]). In our case, the Nullstellensatz proof is the tuple (1 + x 3 , x 1 , 0, 0, 0) because of the equality (1 + x 3 )(x 1 + x 1 x 2 ) + x 1 (x 2 + x 2 x 3 ) = x 1 + x 1 x 3 . Now we write the polynomials f 1 , f 2 as F 1 = {x 1 , 1 + x 2 } and F 2 = {x 2 , 1 + x 3 } . Resolving on x 2 yields H = {x 1 , 1+x 3 } which correponds to the polynomial h. Note that the maximal degree in the proof is now 2, and the SRES proof is simpler than the Gröbner proof.
Further typical examples that are easy for SRES and difficult for resolution [13] are inconsistent systems of linear equations. By Proposition 12, SRES simulates the addition rule, and thus one can use Gaußian elimination to produce SRES-refutations for such systems. Recall the encoding into linear clauses in Example 16 is very efficient for SRES, but multiplying out the products causes an exponential blowup. A similar problem emerges in the next example in the case of CNF encodings.
Example 25 Consider the linear system
over F 2 . On one hand, encoding f 1 and f 2 in CNF suffers from introducing either exponentially many auxiliary variables or exponentially many new clauses. On the other hand, by the weakening rule and 2 -resolution we get f 1 (f 2 + 1) + (f 1 + 1)f 2 = 1 in B n immediately.
Let us conclude this section and this paper with a few remarks about the problem that is solved by Algorithm 3. The traditional way in Computer Algebra is to use Gröbner basis algorithms. As we saw in Example 16, they have serious drawbacks in our setting and tend to run out of memory quickly.
Another approach is to use a SAT solver, e.g. a version of the DPLL algorithm. However, the DPLL approach needs a huge number of clauses to describe XOR constraints. All in all, the classical DPLL algorithm can be extended to linear clauses in a rather straightforward way, as for instance done in [7], but appears to be not very efficient.
The new approach introduced here, namely the SRES proof system and the SRES Refutation Algorithm, offers the prospect of a new and tailor-made way to treat systems of linear clauses. Besides finding possible optimizations of the implementation, we may enhance it further by combining it with a suitable conflict-learning mechanism such as the ones which lie at the heart of modern SAT solvers. Recall that conflict clauses in SAT solvers can be generated from 1 -resolvents of a cut in the implication graph. Thus, s -resolution may generalize conflict learning in the case of linear clauses or help to improve a separate XORreasoning module such as one introduced in [9].
Acknowledgments. The authors thank Jan Krajíček and Iddo Tzameret for fruitful discussions on combined proof systems. We thank the anonymous reviewers for their many insightful comments. This work was financially supported by the DFG project "Algebraische Fehlerangriffe" [KR 1907/6-2].