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 2 hSi . Traditionally, one can use Grobner 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
Grobner basis algorithms, namely the s -resolvents we introduced in [
From the propositional logic point of view, we would like to decide if the
semantic implication S j= f holds. Recall that a linear Boolean polynomial
xi1 + + xij corresponds to a linear XOR constraint xi1 xij . Such
constraints are very di cult for SAT solvers because the truth value depends
genuinely on all variables, i.e., changing the value of one variable results in
ipping 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 [
The paper is organized as follows. In Section 2 we recall the de nition 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 de ne the proof system SRES which incorporates and
extends the s -resoution rule de ned in [
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 de nitions and results given in [
Let F2 = Z=2Z be the binary eld and F2[x1; : : : ; xn] a polynomial ring over F2 . The ring Bn = F2[x1; : : : ; xn]=F with F = hx12 + x1; : : : ; x2n + xni is called the ring of Boolean polynomials in the indeterminates x1; : : : ; xn . Let Ln be the set of all linear polynomials in F2[x1; : : : ; xn] , 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 2 Ln : (C1) A set of linear polynomials H = f`1; : : : ; `kg Ln . (C2) A Boolean polynomial h = Qk
i=1 `i which is a product of linear polynomials in Bn . (C3) A linear clause (`1 = 0) _ _ (`k = 0) .
Example 1 Let H = fx1 + x2 + 1; x1 + x3g L3 . Then h = (x1 + x2 + 1)(x1 + x3) = x1x3 + x1x2 + x2x3 + x3 , and H (resp. h ) coresponds to the propositional logic formula (x1 x2 1 = 0) _ (x1 x3 = 0):
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 [
The subsets in (C1) are measured by degree and size. We recall here some
de nitions from [
De nition 3 Let H = f`1; : : : ; `kg
Ln . (1) The number deg(h) = #H is called the degree of H . (2) For ` 2 Ln , 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 unsatis able. For this purpose, we de ne semantic implication as follows. De nition 4 Let F1; : : : ; Fm; H Ln . We say that F1; : : : ; Fm semantically imply H if every F2 -rational common zero of the Boolean polynomials corresponding to F1; : : : ; Fm is a zero of H . In this case we write F1; : : : ; Fm j= H .
From the algebraic point of view, we have F1; : : : ; Fm j= H if and only if H 2 hF1; : : : ; Fmi Bn . Note that the zeros of an ideal in Bn are always F2 rational, because ideals in Bn correspond to ideals in F2[x1; : : : ; xn] that contain the eld ideal hx12 + x1; : : : ; x2n + xni . Using the newly de ned 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 f g 1 . 3
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 Grobner proof system de ned in [
g f + g (Pa) and
(Pm) f xif where f; g 2 F2[x1; : : : ; xn] and xi is an indeterminate.
In this section we continue to study the proof system based on s -resolution
which was introduced in [
De nition 5 The proof system s-resolve is de ned by the following parts: (1) A formula is a set of linear polynomials f`1; : : : ; `sg Ln , where s 2 N+ . (2) The axioms are the Boolean axioms given by fxi; xi + 1g for i = 1; : : : ; n . (3) There exists one rule of inference (R) , namely
Sis=1f`ig [ G
Sis=1f`i + 1g [ G~ Sis=11f`i + `i+1 + 1g [ G [ G~ (R) where G; G~
Ln and s 1 . This rule is also called s -resolution. (For s = 1 , we let Sis=11f`i + `i+1 + 1g = ; .) 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 fxi; xi + 1g and fxi + 1; xig , we obtain that f0g is a tautology in the s -resolve proof system.
In [
De nition 7 Let (I) be a rule of inference of a proof system. We say that the rule of inference (I) is correct if
F1
F2 : : :
Fm H (I) for some formulas F1; : : : ; Fm; H implies F1; : : : ; Fm j= H .
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. Example 8 Resolving two sets F = fx1 + 1; x1 + x3; x1 + x2 + 1; x2 + x3 + 1g and G = fx1; x1 + x3 + 1; x1 + x2; x2 + x3g with the numbering `1 = x1 + 1 , `2 = x1 + x3 , `3 = x1 + x2 + 1 , `4 = x2 + x3 + 1 yields the 4-resolvent R1 = fx3; x2 + x3; x1 + x3 + 1g . If we swap the last two polynomials in G , 4 -resolution with the numbering `1 = x1 + 1 , `2 = x1 + x3 , `4 = x1 + x2 + 1 , `3 = x2 + x3 + 1 yields R2 = fx3; x1 + x2; x1 + x3 + 1g . Both R1 and R2 correspond to the same Boolean polynomial, as we saw in Example 2.
Next we enrich s -resolve with a new rule of inference as follows. De nition 9 The proof system SRES is de ned by the following parts. (1) The syntax agrees with the syntax of s -resolve, i.e. a formula is a set of linear polynomials f`1; : : : ; `sg Ln , where s 2 N+ . (2) The axioms are the Boolean axioms fxi; xi + 1g for i = 1; : : : ; n . (3) The rules of inference consist of s -resolution (R) and the following weakening rule (W) : De nition 10 Let PS be a proof system. A PS-proof of a formula H from the initial premises F1; : : : ; Fm in the proof system PS is a sequence of formulas = (G1; : : : ; Gk) such that Gk = H and each of the formulas Gi is of one of the following forms: (1) Gi 2 fF1; : : : ; Fmg (2) Gi is one of the axioms of PS. (3) Gi is obtained from some of the formulas Gj 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 fF1; : : : ; Fmg , we write F1; : : : ; Fm `PS H , or simply F1; : : : ; Fm ` H if no confusion can arise.
Since the proof system SRES is correct, our goal to refute fF1; : : : ; Fmg can now be expressed by asking that we should prove F1; : : : ; Fm ` f g 1 . Notice that the intended semantics is that an unsatis able formula corresponds to polynomial equations `i;1 `i;s = 0 for i 2 f1; : : : ; mg which has no solution. Equivalently, a tautology is an equation which holds for all points of F2n . 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.
De nition 11 Let F; G be subsets of Ln , and let `; `1; `2 2 Ln . (1) The rule (U ) de ned by
is called unit cancellation. (2) The rule (MP) de ned by
H [ f1g
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 [ f1g and f0g , and we get H . To prove modus ponens it su ces to use (R) with s = 1 and G = ; . Finally, we show the correctness of (A) . Using the weakening rule, we infer F [ f`1; `2 + 1g from F [ f`1g and H [f`2; `1 +1g from H [f`2g . Then, using 2 -resolution, we get F [H [f`1 +`2g . tu
The following remark and the subsequent proposition will become important later in the proof of Proposition 18.
Remark 13 Let = (H1; : : : ; Hk) be an SRES-proof of Hk from F1; : : : ; Fm that uses only the s -resolution rule. Let ` be an element of one of the sets Hi . Then ` lies in the F2 -vector space generated by the linear polynomials contained in the union Sim=1 Fi .
Proposition 14 Let F Ln and let i 2 f1; : : : ; ng . For a 2 f0; 1g , let F (xi 7! a) denote the set which is obtained by substituting xi 7! a into the linear polynomials contained in F . Then the following claims hold true for i 2 f1; : : : ; ng . (1) F; fxig `SRES F (xi 7! 0) (2) F (xi 7! 0); fxig `SRES F (3) F; fxi + 1g `SRES F (xi 7! 1) (4) F (xi 7! 1); fxi + 1g `SRES F Proof. First we prove (1). Let ` 2 F be such that xi occurs in ` . The polynomial xi + ` corresponds to substituting xi = 0 into ` . This addition can be derived in SRES using Proposition 12. The claims (2){(4) follow analogously from Proposition 12. tu
The next example illustrates this proposition.
Example 15 Let F1 = fx1 + x2; x1g and F2 = fx1 + 1g . By Proposition 12, there exists an SRES-proof of the set fx2 + 1; 1g from F1; F2 which corresponds to the substitution of x1 = 1 into F1 . On the other hand, we can \backtrack" the substitution, i.e. we have F2; fx2 + 1; 1g `SRES F1 .
The following example shows an important advantage of the SRES proof
system over the Grobner proof system de ned in [
F1 = fx1 + x2; : : : ; xn + xn+1g F2 = fx1 + x2 + 1g F3 = fx2 + x3 + 1g ... = ...
Fn+1 = fxn + xn+1 + 1g
On one hand, it is easy to see that the system is inconsistent because substituting F2; : : : ; Fn+1 into F1 gives us 1 . On the other hand, the input for the Grobner basis algorithm is assumed to be expanded (i.e., not in the form of products of linear polynomials). We can always nd n 2 N such that expanding F1 to the polynom f1 = Qin=1(xi + xi+1) , which has 2n terms, exceeds the available memory, and hence any Grobner basis algorithm can not be applied. Notice that we have size(F1) = 2n .
One workaround would be to introduce new indeterminates to break the long product, but it does not help too much because the Grobner basis algorithm substitutes the new indeterminates back, and thus recovers the expanded polynomial F1 again.
However, by Proposition 14, there exists a short SRES refutation that corresponds to the substitution of F2; : : : ; Fn+1 into F1 .
The following de nition provides further useful properties of proof systems. De nition 17 (1) A proof system is called implicationally complete if for every formula H and every set of formulas fF1; : : : ; Fmg such that we have F1; : : : ; Fm j= H , there exists a proof of H from F1; : : : ; Fm in this proof system. (2) A proof system is called refutationally complete if for every inconsistent set of formulas fF1; : : : ; Fmg , i.e. for F1; : : : ; Fm j= f1g , there exists a proof of f1g from F1; : : : ; Fm 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 F1; : : : ; Fm; H Ln be sets of linear polynomials such that F1; : : : ; Fm j= H . We want to prove that F1; : : : ; Fm `SRES H . We proceed by induction on the number k = size(F1) + + size(Fm) + size(H) .
Let us consider the case k = 0 , i.e. the case when all linear polynomials in Fi and H are constants 0 or 1. If all sets F1; : : : ; Fm are equal to f0g , there is trivially an SRES-proof of f0g . All the semantic implicants of f0g of size 0 can be derived from f0g by the weakening rule. If there exists a set Fi = f1g , then there is trivially an SRES-proof that refutes F1; : : : ; Fm , and hence we can derive any linear clause by the weakening rule and the unit cancellation rule. Finally, if Fi = f0; 1g , then Fi is simpli ed to f0g 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
F1; : : : ; Fm j= H in which the sum of sizes of F1; : : : ; Fm; H is at most k+1 . Choose i 2 f1; : : : ; ng such that xi occurs in F1 [ [ Fm [ H . Given a 2 f0; 1g , let F (xi 7! a) denote the set which is obtained by substituting xi 7! a into the linear polynomials contained in F .
By Proposition 14, we have Fj ; fxig `SRES Fj (xi 7! 0) for j = 1; : : : ; m . Moreover, we clearly have F1(xi 7! 0); : : : ; Fm(xi 7! 0) j= H(xi 7! 0) . By the induction hypothesis, there is an SRES-proof of H(xi 7! 0) from F1(xi 7! 0); : : : ; Fm(xi 7! 0) . Altogether, we get
fxig; F1; : : : ; Fm `SRES H(xi 7! 0):
Furthermore, by Proposition 14, we have H(xi 7! 0); fxig `SRES H . All in all, there is an SRES-proof 1 of H from fxig; F1; : : : ; Fm . Analogously, we get an SRES-proof 2 of H from fxi + 1g; F1; : : : ; Fm .
Next we modify the derivations of 1 (resp. 2 ) such that they start from fxi; xi + 1g; F1; : : : ; Fm instead of fxig; F1; : : : ; Fm (resp. fxi + 1g; F1; : : : ; Fm ). Note that the same rules of inference can be applied, and thus one can rewrite the proof 1 into an SRES-proof 1 from fxi; xi + 1g; F1; : : : ; Fm of either H or H [ fxig . Similarly, we rewrite 2 into an SRES-proof 2 from fxi; xi + 1g; F1; : : : ; Fm of H or H [ fxi + 1g . If the proof 1 or 2 ends with H , we are done. Otherwise, we have H [ fxig; H [ fxi + 1g `SRES H by a single step of the 1 -resolution rule, which concludes the proof. tu
The SRES proof system is in fact a combined proof system in the sense of [8,
Sec.7.1]. For instance, R(lin) in [
On the other hand, SRES cannot simulate the rule (Pa) of the Grobner proof system because addition of two products of linear polynomials does not have to be a product of linear polynomials in Bn , e.g., x1 x2 + 1 cannot be written as a product of linear polynomials in B3 . 4
In [
Input: Sets F; G Ln . We assume that #f` 2 F j ` + 1 2 Gg 1 . Output: A set R Ln such that R is the s -resolvent of F and G .
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 de ned as follows.
following two conditions hold for all (F 0; G0) 2 K (1) #f` 2 F 0 j ` + 1 2 G0g (2) F 0 [ G0
F [ G [ f` + 1 j ` 2 F [ Gg is called the set of expansions for F; G .
Condition (1) encodes the fact that there exists at least one ` 2 Ln in F 0 and G0 on which we can s -resolve. Condition (2) restrains F 0; G0 to contain linear polynomials ` or ` + 1 such that ` 2 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 ful lled because of the two foreach loops in Steps 3, 4.
Algorithm 2 AllExpansions (All Possible Expansions to s -Resolution) Input: Sets F; G Ln .
Output: The set of expansions for F; G .
The next example shows the generation of the pairs in Algorithm 2. Example 20 Let F = fx1; x2; x3 + 1g and G = fx1 + 1; x2; x4g . Then we may extend F to F itself, to fx1; x2; x3 + 1; x4g , or to fx1; x2; x3 + 1; x4 + 1g . Similarly, we may extend G to G , to fx1 + 1; x2; x4; x3 + 1g , or to fx1 + 1; x2; x4; x3g . Altogether, nine pairs are constructed.
Next we process the pairs computed by Algorithm 2 in increasing order with respect to the following ordering relation.
De nition 21 Let F; G; F1; F2; G1; G2 Ln . (1) We write F G if we have deg(F ) < deg(G) , or if we have deg(F ) = deg(G) and size(F ) < size(G) . (2) Let #f` 2 F1 j ` + 1 2 G1g 1 and #f` 2 F2 j ` + 1 2 G2g (F1; G1) E (F2; G2) if Sres(F1; G1) Sres(F2; G2) .
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.
Algorithm 3 SRES Refute (SRES Refutation Algorithm) Input: Subsets F1; : : : ; Fm Ln such that Fi does not contain any duplicate elements.
Output: False if F1; : : : ; Fm j= f1g , True otherwise.
Require: Algorithms 1, 2. Proposition 22 Algorithm 3 is correct, refutationally complete, and nite. In particular, the algorithm returns False if and only if F1; : : : ; Fm j= f1g . Proof. Finiteness follows from the fact that there are only nitely many linear polynomials in Ln . Hence the sets in S are nite, and so is the set P Ln Ln .
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 F1; : : : ; Fm . 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 2 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 F1; : : : ; Fm . 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 f1g is eventually discovered by the algorithm. tu
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.
Example 23 Let F1 = fx1 + 1g and F2 = fx1; x2g . Algorithm AllExpansions outputs (F1; F2) , (F1 [ fx2 + 1g; F2) , (F1 [ fx2g; F2) . The pair (F1 [ fx2g; F2) can be stored as a tuple (1; fx2g; 2; ;; 1) with the meaning \Sres of F1 [ fx2g and F2 [ ; 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. 5
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 [
In the following example taken from [
i j Example 24 Consider the polynomials f1 = x1 + x1x2 and f2 = x2 + x2x3 in F2[x1; x2; x3] . They encode two implications x1 ! x2 and x2 ! x3 . (E.g., if x1 = 1 , then x2 is constrained to be 1.) Let us write a proof of h = x1 + x1x3 , i.e., the implication x1 ! x3 , in the Grobner proof system.
Firstly, we multiply f2 by x1 , and we get g1 = x1x2 + x1x2x3 . The addition f1 + g1 gives us x1 + x1x2x3 . Then we compute g2 = x3 f1 = x1x3 + x1x2x3 . Finally, we get g1 + g2 = x1 + x1x3 .
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
x1 ! xn from x1 ! x2; : : : ; xn 1 ! xn (see [
(1 + x3)(x1 + x1x2) + x1(x2 + x2x3) = x1 + x1x3:
Now we write the polynomials f1; f2 as F1 = fx1; 1 + x2g and F2 = fx2; 1 + x3g . Resolving on x2 yields H = fx1; 1+x3g 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 Grobner proof.
Further typical examples that are easy for SRES and di cult for
resolution [
f1 = x1 + + xn; f2 = x1 + + xn + 1 over F2 . On one hand, encoding f1 and f2 in CNF su ers 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 f1(f2 + 1) + (f1 + 1)f2 = 1 in Bn 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 Grobner 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 [
The new approach introduced here, namely the SRES proof system and the
SRES Refutation Algorithm, o ers the prospect of a new and tailor-made way
to treat systems of linear clauses. Besides nding possible optimizations of the
implementation, we may enhance it further by combining it with a suitable
con ict-learning mechanism such as the ones which lie at the heart of modern
SAT solvers. Recall that con ict clauses in SAT solvers can be generated from
1 -resolvents of a cut in the implication graph. Thus, s -resolution may generalize
con ict learning in the case of linear clauses or help to improve a separate
XORreasoning module such as one introduced in [
Acknowledgments. The authors thank Jan Kraj cek and Iddo Tzameret for fruitful discussions on combined proof systems. We thank the anonymous reviewers for their many insightful comments. This work was nancially supported by the DFG project \Algebraische Fehlerangri e" [KR 1907/6-2].