key: cord-0046672-2k7bbnup
authors: Chew, Leroy; Heule, Marijn J. H.
title: Sorting Parity Encodings by Reusing Variables
date: 2020-06-26
journal: Theory and Applications of Satisfiability Testing - SAT 2020
DOI: 10.1007/978-3-030-51825-7_1
sha: e0f5ffb0c8e2c7de1ba36d1f9e69577d3f62851a
doc_id: 46672
cord_uid: 2k7bbnup

Parity reasoning is challenging for CDCL solvers: Refuting a formula consisting of two contradictory, differently ordered parity constraints of modest size is hard. Two alternative methods can solve these reordered parity formulas efficiently: binary decision diagrams and Gaussian Elimination (which requires detection of the parity constraints). Yet, implementations of these techniques either lack support of proof logging or introduce many extension variables. The compact, commonly-used encoding of parity constraints uses Tseitin variables. We present a technique for short clausal proofs that exploits these Tseitin variables to reorder the constraints within the DRAT system. The size of our refutations of reordered parity formulas is [Formula: see text].

Modern SAT solving technology is based on Conflict Driven Clause Learning (CDCL) [12] . The resolution proof system [16] has a one-to-one correspondence [15] with CDCL solving. In practice, however, the preprocessing techniques used in modern solvers go beyond what can be succinctly represented in a resolution proof. As a consequence, when we need to present verifiable certificates of unsatisfiable instances, resolution is not always sufficient. Extended Resolution (ER) [20] is a strong proof system that can polynomially simulate CDCL and many other techniques. However, ER is not necessarily the most useful system in practice, as we also want to minimise the degree of the polynomial simulation. The DRAT proof system [7] is polynomially equivalent to ER [8] . Yet most practitioners favour DRAT due to its ability to straightforwardly simulate known preprocessing and inprocessing techniques. DRAT works by allowing inference to go beyond preserving models and instead preserves only satisfiability.

In this paper, we demonstrate DRAT's strengths on a particular kind of unsatisfiable instances that involve parity constraints. Formulas with parity constraints have been benchmarks for SAT for decades. The Dubois family encodes the refutation of two contradictory parity constraints over the same variables using the same variable ordering. Urquhart formulas [21] encode a modulo two sum of the degree of each vertex of a graph, the unsatisfiability comes from an assertion that this sum is odd, a violation of the Handshake Lemma. The Parity family from Crawford and Kearns [3] takes multiple parity instances on a set of variables and combines them together. For these problems, practical solutions have been studied using Gaussian elimination, equivalence reasoning, binary decision diagrams and other approaches [5, 6, [9] [10] [11] 13, 18, 19, 22] .

Extracting checkable proofs in a universal format has been another matter entirely. While it is believed that polynomial size circuitry exists to solve these problems, actually turning them into proofs could mean they may only be "short" in a theoretical polynomial-size sense rather than a practical one. Constructing a DRAT proof of parity reasoning has been investigated theoretically [14] , but no implementation exists to actually produce them nor is it clear whether the size is still reasonable to be useful in practice.

There has been some investigation into looking at DRAT without the use of extension variables. DRAT − , which is DRAT without extension variables, is somewhere in between resolution and ER in terms of power. Several simulation results for DRAT − [2] , show that it is a powerful system even without the simulation of ER. A key simulation technique was the elimination and reuse of a variable, which we use to find short DRAT − proofs of a hard parity formula.

The structure of parity constraints can be manipulated by reusing variables and we exploit the associativity and commutativity of the parity function. We demonstrate this on formulas similar to the Dubois family except the variables now appear in a random order in one parity constraint. We show how to obtain DRAT proofs of size O(n log n) without using additional variables. Our method can also be used to produce ER proofs of similar size with new variables.

In propositional logic a literal is a variable x or its negation x, a clause is a disjunction of literals and a Conjunctive Normal Form (CNF) is conjunction of clauses. A unit clause is a clause containing a single literal. We denote the negation of literal l as l (or ¬l). The variable corresponding to literal l is var(l). If C is a clause, then C is the conjunction of the negation of the literals in C each a unit clause. In this paper, we treat clauses/formulas as unordered and not containing more than one copy of each literal/clause respectively.

Unit propagation simplifies a conjunctive normal form F by building a partial assignment and applying it to F . It builds the assignment by satisfying any literal that appears in a unit clause. Doing so may negate opposite literals in other clauses and result in them effectively being removed from that clause. In this way, unit propagation can create more unit clauses and can keep on propagating until no more unit clauses remain or the empty clause is reached. We denote that the empty clause can be derived by unit propagation applied to CNF F by F 1 ⊥. Since unit propagation is an incomplete but sound form of logical inference this is a sufficient condition to show that F is a logical contradiction. The DRAT proof system. Below we define the rules of the DRAT proof system. Each rule modifies a formula by either adding or removing a clause while preserving satisfiability or unsatisfiability, respectively. [7] ). Let F be a CNF formula. A clause C is an asymmetric tautology w.r.t. F if and only if F ∧ C 1 ⊥.

Asymmetric tautologies are also known as RUP (reverse unit propagation) clauses. The rules ATA and ATE allow us to add and eliminate AT clauses. ATA steps can simulate resolution steps and weakening steps.

The rules RATA and RATE allow us to add and eliminate RAT clauses. RATA can be used to add new variables that neither occur in F or anywhere else. This can be used to simulate extension steps in ER.

In this section we will detail the main family of formulas investigated in this work. These formulas will be contradictions expressing both the parity and nonparity on a set of variables.

We define the parity of propositional literals a, b, c as follows

. , x n }, and let σ be a bijection between literals on X, that preserves negation (σ(¬l) = ¬σ(l)). Let e denote the identity permutation on the literals of X. Let T = {t 1 , . . . , t n−3 }. We define Parity(X, T, σ) as

This formula is satisfiable if and only if the total parity of {σ(x i ) | x i ∈ X} is 1. The T variables act as Tseitin variables and whenever the formula is satisfied t i+1 is the sum modulo two of σ(x 1 ), . . . , σ(x i+2 ). The final clauses, xor(t n−3 , σ(x n−1 ), σ(x n )) thus are satisfied when the sum of t n−3 , σ(x n−1 ) and σ(x n ) is 1 mod 2. Suppose we pick σ so that there is some i ∈ [n] such that σ(x j ) is a negative literal if and only if j = i. Let T = {t 1 , . . . , t n−3 } be another set of Tseitin variables. Parity(X, T, σ) ∧ Parity(X, T , e) is false as it states the parity of X is true but also states it false. However the permutation σ obfuscates the similarities between the two Parity parts of the formula.

Were σ(x j ) = x j for all j = i and σ(x i ) = −x i then these formulas would be equivalent to the Dubois formulas and a linear proof could be made by inductively deriving clauses that express t j = t j for j < i − 1 and then t j = t j for j ≥ i − 1. This will always allow us to derive a contradiction. While a linear resolution proof is known for the Dubois, it is unknown what the size of the shortest resolution proof of Parity(X, T, σ) ∧ Parity(X, T , e) for a random σ. While the Dubois family are a special case of these formulas, these formulas are in turn a special case of the Tseitin graph formulas [20] where the vertex degree is always 3.

When σ = e we still have a contradiction due to the commutativity of the parity function. However such a straightforward DRAT proof becomes obstructed by the disarranged ordering. This permutation also makes these formulas hard for CDCL solvers (see Section 4). We will show that Parity(X, T , e) can be efficiently reordered. Afterwards a short resolution proof arises. This brings us to our main theoretical result. In the remainder of this section we will prove Theorem 1. We begin with an essential lemma that uses the DRAT rules to perform elementary adjacent swaps on literals in xor constraints. F and two sets of xor clauses xor(a, b, p) and xor(p, c, q), where variable p appears nowhere in F . We can infer xor(b, c, p) ∧ xor(p, a, q) in a constant number of DRAT steps without adding new variables.

Proof. The idea is to eliminate variable p so that we define q directly as the parity of a, b, c using eight "ternary xor" clauses. Each of these clauses can be added directly via ATA. We can now remove (using RATE) all clauses that contain variable p. These steps are equivalent to performing Davis-Putnam (DP) resolution [4] on variable p.

What we are left with is that two levels of parity have been replaced with one level of ternary parity. We can reverse the above steps to get us two levels of parity yet again, but we can swap a and c (since they appear symmetrically in our "ternary xor" clauses). We re-use the eliminated p to now mean the xor of b and c using RATA. Finally, we remove the "ternary xor" clauses using ATE.

Note that here elimination is required only because we want to re-use the variable p. We can also show a similar step in ER without the elimination steps, introducing the "ternary xor" clauses immediately with resolution. We can introduce the four xor(p , b, c) extension clauses for p , and by resolving them with the ternary clauses on b we get eight intermediate clauses which can resolve with each other on c to get the remaining four xor(p , a, q) clauses. Without ATA and RATA steps, this process involves 50% more addition steps, but since it contains no deletion steps we have 25% fewer steps in total. ER proofs allow us to keep lemmas without deletion so where we have more than two parity constraints we may wish to reuse derived parity clauses. On the other hand DRAT − keeps the number of variables and clauses fixed when searching when we do not know the structure of formula and can stop the search size from growing.

Sorting the input literals. We can switch the two parity inputs using Lemma 1 in a constant number of proof steps. Furthermore the technique in DRAT does not require any additional extension variables and since the number of addition and deletion steps in Lemma 1 is the same, the working CNF does not change in size. Sorting using adjacent variables requires Θ(n 2 ) swaps.

Let us ignore the variables x n−1 and x n and the clauses that include them as special cases. We can take xor(x 1 , x 2 , t 1 ) ∧ n−4 i=1 xor(t i , x i+2 , t i+1 ) as the definition of t n−3 in circuit form, using the X variables as input gates and the t i variables as xor (⊕) gates. This circuit is a tree with linear depth. the distance between two input nodes is linear in the worst-case, which is why we get Ω(n 2 ) many swaps. However Lemma 1 allows us even more flexibility, we can not only rearrange the input variables but the Tseitin variables.

For example if we have xor(t i , x i+2 , t i+1 ) and xor(t i−1 , x i+1 , t i ) clauses we can eliminate t i so that t i+1 is defined as the parity of x i+1 , x i+2 , and t i−1 . However we can now redefine t i as the xor of x i+1 , x i+2 (using xor(t i , x i+1 , x i+2 )) and t i+1 as the xor of t i and t i−1 (using xor(t i+1 , t i , t i−1 )). See Figure 2 for an example and notice how we change the topology of the tree.

In n 2 many swaps we can change our linear depth tree into a tree that consists of a two linear branches of depth at most n 2 joined at the top by an xor. This means that using a divide and conquer approach, we can turn this tree in a balanced binary tree of log 2 n depth in O(n log n) many steps.

The purpose of a log depth tree structure is to allow leaf-to-leaf swapping from both ends of the the tree without having to do a linear number of swaps, in fact we can do arbitrary leaf swaps in O( log n ) many individual steps. This is done by pushing a variable up its branch to the source node of the tree and pushing it back down another branch to its destination as in Figure 3 . Then we can reverse the steps with the variable being swapped out. The resulting tree even retains the position of all other nodes.

Note that we also have the variables x n and x n−1 that only appear in the clauses of xor(t n−3 , x n−1 , x n ). Suppose the two children of t n−3 in its definition circuit are a and b, in other words xor (t n−3 , a, b) are the clauses currently defining t n−3 . Without loss of generality suppose we want to swap x n−1 with a.

The clauses of xor(t n−3 , x n−1 , x n ) are exactly the same as the clauses of xor(t n−3 , x n−1 , x n ). Using Lemma 1 we can eliminate t n−3 and gain eight clauses that represent that x n is the ternary xor of a, b and x n−1 . Then we can reverse the steps but instead swap the positions of x n−1 and a.

In this way we can introduce x n−1 or x n into the tree and swap it with any leaf. Once again we only require O(log n) many applications of Lemma 1 to completely swap the position of x n−1 or x n with any leaf.

Arriving at the empty clause. The total number of leaf-to-leaf swaps we are required to perform is bounded above linearly so we stay within O(n log n) many steps. We can now undo the balanced tree into a linear tree in (we reverse what we did to balance it) keeping within an O(n log n) upper bound.

Recall that we performed a sort on the variables in Parity(X, T , e) thereby transforming it into Parity(X, T , σ ) with var(σ (x)) = var(σ(x)), resulting in the formula Parity(X, T, σ) ∧ Parity(X, T , σ ). Thus the final part of the proof now involves refuting a formula equivalent to one of the Dubois formulas.

We create a proof that inductively shows equivalence or non-equivalence between variables t j ∈ T and the t j ∈ T starting from j = 1 to j = n − 3. If there is an even number of instances i,

Whichever case, we can increase j with the addition (ATA) of six clauses. We can think of this as working via DP resolution in a careful order: σ(x j+1 ), t j−1 , t j from j = 1 to n − 3 in increasing j (and treat σ(x 1 ) as t 0 ).

Finally, when j = n − 3, we have either already exceeded the single value i such that σ (x i ) = σ(x i ), or it appears in n − 1 or n. Either way, we can add the four clauses (σ(x n−1 ) ∨ σ(x n )), (¬σ(x n−1 ) ∨ σ(x n )), (σ(x n−1 ) ∨ ¬σ(x n )), (¬σ(x n−1 ) ∨ ¬σ(x n )) then the two unit clauses (σ(x n )) and (¬σ(x n )) and finally the empty clause. This final part of the refutation uses O(n) many ATA steps.

The formulas we ran experiments on are labelled rpar(n, g). Which represent Parity(X, T, σ (n,g) ) ∧ Parity(X, T , e) using the DIMACS format. The parameter n is the number of input variables and a random number generator g. The CNF uses variables X = {1, . . . , n}, T = {n + 1, . . . , 2n − 3}, T = {2n − 2, . . . , 3n − 6}, e is the identity permutation, and σ (n,g) is a random permutation based on g, where one random literal i n,g is flipped by σ.

We ran a program rParSort that generated an instance rpar(n, rnd s ) based on a seed s and also generated a DRAT proof based on Theorem 1. We compare the size of our proofs by ones produced by the state-of-the-art SAT solver CaDiCaL [1] (version 1.2.1) and the tool EBDDRES [17] (version 1.1). The latter solves the instance using binary decision diagrams and turns the construction into an ER proof. These ER proofs can easily be transformed into the DRAT format as DRAT generalizes ER. Proof sizes (in the number of DRAT steps, i.e. lines in the proof) are presented and compared in Figure 4 .

rParSort proofs remained feasible for values as large as n = 4000 with proofs only being 150MB due to the O(n log n) upper bound in proof lines. We believe n vars clauses lines size (KB)   10  24  64  1 681  25  20  54  144  7 469  115  50  144  384  30 657  481  101  297  792  77 leading coefficient is also kept small by number of factors such as the proof lines being width 4 and only 16 being needed per swap step.

CaDiCaL showed difficulty for modest values of n. While proofs with less than 10 6 lines are common for n = 35, the size and running time grows exponentially and by n = 41 proofs are larger than 10 7 lines. CaDiCaL times out using a 5000 seconds limit on some instances with n = 46 and on most instances with n ≥ 50.

The size of proofs produced by EBDDRES appears to grow slower compared to CDCL, which is not surprising as BDDs can solve the formulas in polynomial time. However, as can be observed in Figure 4 , the ER proofs are actually bigger for small n. The extracted DRAT proofs (converted from the ER proofs) are large: the average proof with n ≥ 35 had more than 10 7 lines. This means that this BDD-based approach is not practical to express parity reasoning in DRAT.

We have shown that through manipulating existing encoding variables DRAT can take advantage of the commutativity of xor definitions via Lemma 1. Our proof generator is capable of producing reasonable-sized proofs for instances with tens of thousands of variables, while state-of-the-art SAT solvers without xor detection and Gaussian elimination, such as CaDiCaL, can only solve instances up to about 60 variables. Although these formulas are also doable for BDD-based approaches, the resulting proofs are too big for practical purposes.

The DRAT proofs are in the fragment of DRAT − , where the number of variables stays fixed, which is of potential benefit to the checker. If we are not concerned with the introduction of new variables, our DRAT proofs can easily be made into ER proofs with only a 50% increase in addition steps (and the introduction of new variables). This is an alternative approach that may prove useful in other settings where elimination of a variable is not so easy.

CaDiCaL at the SAT Race

DRAT proofs, propagation redundancy, and extended resolution

The minimal disagreement parity problem as a hard satisfiability problem

A computing procedure for quantification theory

When Boolean satisfiability meets Gaussian elimination in a simplex way

Aligning CNF-and equivalence-reasoning

Inprocessing rules

Extended resolution simulates DRAT

Extending clause learning DPLL with parity reasoning

Equivalence class based parity reasoning with DPLL(XOR)

Equivalent literal propagation in the DLL procedure

Conflict-driven clause learning SAT solvers

Recovering and exploiting structural knowledge from CNF formulas

DRAT proofs for XOR reasoning

On the power of clause-learning SAT solvers as resolution engines

Theorem-proving on the computer

Extended resolution proofs for conjoining BDDs

Enhanced Gaussian elimination in DPLL-based SAT solvers

Extending SAT solvers to cryptographic problems

On the complexity of derivations in propositional calculus

Hard examples for resolution

A two-phase algorithm for solving a class of hard satisfiability problems

Acknowledgements. The authors thank Armin Biere for his useful comments on an earlier draft. This work has been support by the National Science Foundation (NSF) under grant CCF-1618574.