# certifying_parity_reasoning_efficiently_using_pseudoboolean_proofs__63e90987.pdf

Certifying Parity Reasoning Efﬁciently Using Pseudo-Boolean Proofs

Stephan Gocht,1,2 Jakob Nordstr om,2,1

1 Lund University, Lund, Sweden 2 University of Copenhagen, Copenhagen, Denmark stephan.gocht@cs.lth.se, jn@di.ku.dk

The dramatic improvements in combinatorial optimization algorithms over the last decades have had a major impact in artiﬁcial intelligence, operations research, and beyond, but the output of current state-of-the-art solvers is often hard to verify and is sometimes wrong. For Boolean satisﬁability (SAT) solvers proof logging has been introduced as a way to certify correctness, but the methods used seem hard to generalize to stronger paradigms. What is more, even for enhanced SAT techniques such as parity (XOR) reasoning, cardinality detection, and symmetry handling, it has remained beyond reach to design practically efﬁcient proofs in the standard DRAT format. In this work, we show how to instead use pseudo-Boolean inequalities with extension variables to concisely justify XOR reasoning. Our experimental evaluation of a SAT solver integration shows a dramatic decrease in proof logging and veriﬁcation time compared to existing DRAT methods. Since our method is a strict generalization of DRAT, and readily lends itself to expressing also 0-1 programming and even constraint programming problems, we hope this work points the way towards a uniﬁed approach for efﬁcient machine-veriﬁable proofs for a rich class of combinatorial optimization paradigms.

1 Introduction

Since around the turn of the millennium, combinatorial optimization has been successfully applied to solve an ever increasing range of problems in e.g., resource allocation, scheduling, logistics, and disaster management (Pardalos, Du, and Graham 2013), and more recent applications in biology, chemistry, and medicine (Archibald et al. 2019) include, e.g., protein analysis and design (Allouche et al. 2014; Mann, Will, and Backofen 2008) and kidney transplants (Manlove and O Malley 2012). Yet other examples are government auctions generating billions of dollars in revenue (Leyton-Brown, Milgrom, and Segal 2017), as well as allocation of education and work opportunities (Manlove 2016; Manlove, Mc Bride, and Trimble 2017) and matching of adoptive families with children (Delorme et al. 2019). As more and more such problems are dealt with using combinatorial optimization solvers, an urgent question is whether we can trust that the solutions computed by such

Copyright 2021, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

algorithms are correct and complete. The answer, unfortunately, is currently a clear no : State-of-the-art solvers sometimes return solutions that do not satisfy the constraints or erroneously claim optimality (Cook et al. 2013; Akg un et al. 2018; Gillard, Schaus, and Deville 2019). This can be fatal for applications such as, e.g., chip design, compiler optimization, and combinatorial auctions, where correctness is absolutely crucial, not to speak about when human lives depend on ﬁnding the best solutions. Conventional software testing has made little progress in addressing this problem, and formal veriﬁcation techniques cannot handle the level of complexity of modern solvers. Instead, the most successful approach to date has been that of proof logging in the Boolean satisﬁability (SAT) community, where solvers are required to certify (Mc Connell et al. 2011) their answer by outputting also a simple, machineveriﬁable proof that this answer is correct. This does not certify the correctness of the solver itself, but it does mean that if it ever produces an incorrect answer (even if due to hardware errors), then this can be detected. A number of different proof logging formats such as RUP (Goldberg and Novikov 2003), Trace Check (Biere 2006), DRAT (Heule, Hunt Jr., and Wetzler 2013a,b; Wetzler, Heule, and Hunt Jr. 2014), GRIT (Cruz-Filipe, Marques-Silva, and Schneider Kamp 2017), and LRAT (Cruz-Filipe et al. 2017) have been developed, with DRAT now established as the standard in the SAT competitions (www.satcompetition.org). A quite natural, and highly desirable, goal would be to extend these proof logging techniques to stronger paradigms such as pseudo-Boolean (PB) optimization, Max SAT solving, mixed integer programming, and constraint programming, but such attempts have had limited success. Either the proofs require trusting in powerful and complicated rules (as in, e.g., (Veksler and Strichman 2010)), defeating simplicity and veriﬁability, or they have to justify such rules by long explanations, leading to an exponential slow-down (see (Gange and Stuckey 2019)). In fact, even for SAT solvers a long-standing problem is that more advanced techniques reasoning with parity constraints (XORs), cardinality constraints, and symmetries have remained out of reach for efﬁcient proof logging. Although in theory there should be no problems DRAT is extremely powerful, and can in principle justify such reasoning and much more with at most a polynomial amount of work (Sinz and Biere 2006;

The Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI-21)

Heule, Hunt Jr., and Wetzler 2015; Philipp and Rebola Pardo 2016) in practice the overhead seems completely prohibitive. Thus, a key challenge on the road to efﬁcient proof logging for more general combinatorial optimization solvers would seem to be to design a method that can capture the full range of techniques used in modern SAT solvers.

Our Contribution

In this work, we present a new, efﬁcient proof logging method for parity reasoning that is perhaps somewhat surprisingly based on pseudo-Boolean reasoning with 0-1 linear inequalities. Though such inequalities might seem illsuited to representing XOR constraints, this can be done elegantly by introducing auxiliary so-called extension variables (Dixon, Ginsberg, and Parkes 2004). Using this observation, we strengthen the Veri PB tool recently introduced in (Elffers et al. 2020), which can be viewed as a generalization to pseudo-Boolean proofs of RUP (Goldberg and Novikov 2003). Borrowing inspiration from (Heule, Kiesl, and Biere 2017; Buss and Thapen 2019), we develop stronger, but still efﬁcient, rules that can handle also extension variables, making Veri PB, in effect, into a strict generalization of DRAT. We have implemented our method for representing XOR constraints and performing Gaussian elimination in a library with a simple, clean interface for SAT solvers. As a proof of concept, we have also integrated it in Mini Sat (E en and S orensson 2004), which still serves as the foundation of most state-of-the-art SAT solvers. Our library also provides DRAT proof logging for XORs as described in (Philipp and Rebola-Pardo 2016), but with some optimizations, to allow for a comparative evaluation. Our experiments show that the overhead for proof logging, the size of the produced proofs, and the time for veriﬁcation all go down by orders of magnitude for our method compared to DRAT. Furthermore, the fact that PB reasoning forms the basis for solvers like Sat4j (Le Berre and Parrain 2010) and Rounding Sat (Elffers and Nordstr om 2018) means that our library can also empower such pseudo-Boolean solvers to reason with parities. Since cardinality constraints are just a special case of PB constraints, it is clear that our method should sufﬁce to justify the cardinality reasoning used in SAT solvers. Symmetry reasoning remains a challenge, but at least our method can subsume anything done by DRAT. More excitingly, the original Veri PB tool has already been shown to be capable of efﬁciently justifying a number of constraint programming techniques (Elffers et al. 2020; Gocht, Mc Creesh, and Nordstr om 2020; Gocht et al. 2020). Our optimistic interpretation is that pseudo-Boolean reasoning with extension variables shows great potential as a uniﬁed method of proof logging for SAT solving, pseudo-Boolean optimization, constraint programming, and maybe even mixed integer programming.

Organization of This Paper After some brief background in Section 2, we introduce the key technical notions needed in Section 3 and show how they can be used to justify parity reasoning in Section 4 with a worked out example in Section 5. We present an experimental evaluation in Section 6 and provide some concluding remarks in Section 7.

2 Preliminaries Let us start by quickly reviewing the required material on pseudo-Boolean reasoning, referring the reader to, e.g., (Buss and Nordstr om 2021) for more context. A literal ℓ over a Boolean variable x is x itself or its negation x = 1 x, where variables take values 0 (false) or 1 (true). The set of all literals is denoted Lits. For notational convenience, we deﬁne x = x. A pseudo-Boolean (PB) constraint C is a 0-1 linear inequality P iaiℓi A , (1)

which without loss of generality we always assume to be in normalized form; i.e., all literals ℓi are over distinct variables and the coefﬁcients ai and the degree (of falsity) A are nonnegative integers. We will use equality P iaiℓi = A (2a)

as syntactic sugar for the pair of inequalities P iaiℓi A (2b) P i aiℓi A (2c)

(but rewritten in normalized form) and the negation C of (1) is (the normalized form of) P i aiℓi A + 1 . (3)

A pseudo-Boolean formula is a conjunction F = V j Cj of PB constraints. Note that a clause ℓ1 ℓk is equivalent to the constraint ℓ1 + + ℓk 1, so formulas in conjunctive normal form (CNF) are special cases of PB formulas. A (partial) assignment is a (partial) function from variables to { 0, 1 } and a substitution is a (partial) function from variables to Lits { 0, 1 }. For an assignment or substitution ρ we will use the convention ρ(x) = x for x not in the domain of ρ, denoted x dom(ρ), and deﬁne ρ(x) = 1 ρ(x). We also write x 7 b instead of ρ(x) = b for b Lits { 0, 1 } when ρ is clear from context or is immaterial. Applying ρ to a constraint C as in (1), denoted C ρ, yields the constraint obtained by substituting values for all assigned variables, shifting constants to the right-hand side, and adjusting the degree appropriately, i.e.,

C ρ = P iaiρ(ℓi) A (4)

with appropriate normalization, and for a formula F we deﬁne F ρ = V j Cj ρ. The constraint C is satisﬁed by ρ if P ρ(ℓi)=1 ai A (or, equivalently, if the restricted constraint (4) has a non-positive degree and is thus trivial). A PB formula is satisﬁed by ρ if all constraints in it are, in which case it is satisﬁable. If there is no satisfying assignment, the formula is unsatisﬁable. Two formulas are equisatisﬁable if they are both satisﬁable or both unsatisﬁable. Cutting planes as deﬁned in (Cook, Coullard, and Tur an 1987) is a method for iteratively deriving new constraints C implied by a PB formula F. If C and D are previously derived constraints, or are axiom constraints in F, then any positive integer linear combination of these constraints can be added. We can also add literal axioms ℓi 0 at any time. Finally, from a constraint in normalized form

P i ai ℓi A we can use division by a positive integer d to derive P i ai/d ℓi A/d , dividing and rounding up the degree and coefﬁcients. For PB formulas F, F and constraints C, C , we say that F implies or models C, denoted F |= C, if any assignment satisfying F must also satisfy C, and we write F |= F if F |= C for all C F . It is not hard to see that any collection of constraints F derived (iteratively) from F by cutting planes are implied in this sense, and so it holds that F and F F are equisatisﬁable. A piece of terminology that we will use is that C is implied syntactically by C if C can be derived from C using only addition of literal axioms. A constraint C is said to unit propagate the literal ℓunder ρ if C ρ cannot be satisﬁed unless ℓ7 1. During unit propagation on F under ρ, we extend ρ iteratively by any propagated literals ℓ7 1 until an assignment ρ is reached under which no constraint C F is propagating, or under which some constraint C propagates a literal that has already been assigned to the opposite value. The latter scenario is referred to as a conﬂict, since ρ violates the constraint C in this case, and ρ is called a conﬂicting assignment. Using the generalization of (Goldberg and Novikov 2003) in (Elffers et al. 2020), we say that F implies C by reverse unit propagation (RUP), and write RUP(F, C), if F C unit propagates to conﬂict under the empty assignment. It is not hard to see that RUP(F, C) implies F |= C, but the opposite direction is not necessarily true.

3 Substitution Redundancy In order to provide proof logging for parity reasoning, we need the ability not only to perform cutting planes reasoning, but also to introduce fresh variables not occurring in the formula F under consideration. In particular, we want to be able to use a fresh variable y to encode the reiﬁcation of a constraint P i aiℓi A, i.e., that y is true if and only if the constraint is satisﬁed. We will use the shorthand

y P iaiℓi A (5)

for the two constraints

Ay + P iaiℓi A (6a) A+1+P iai y + P iaiℓi A + 1 + P iai (6b)

enforcing this condition. By way of a concrete example, the reiﬁcation of the constraint

x1 + x2 + x3 2 (7)

using y is encoded as

2y + x1 + x2 + x3 2 (8a) 2y + x1 + x2 + x3 2 (8b)

in pseudo-Boolean form. Note that introducing such constraints maintains equisatisﬁability provided that y does not appear in any other constraint, since depending on whether (7) is satisﬁed or not we can assign y freely to satisfy (8a) or (8b) as needed. More generally, it would be convenient to allow the derivation of any constraint C from F such that F and

F C are equisatisﬁable in which case we say that C is redundant with respect to F regardless of whether F |= C holds or not. A moment of thought reveals that such a completely generic rule would be too good to be true for any unsatisﬁable formula F we would then be able to derive contradiction (say, 0 1) in just one step, and this clearly would not be efﬁciently veriﬁable. What we need, therefore, is a sufﬁcient criterion for redundancy of pseudo-Boolean constraints that is simple to verify. To this end, we generalize the characterization of redundancy in (Heule, Kiesl, and Biere 2017; Buss and Thapen 2019) from CNF formulas to PB formulas as follows. Proposition 1 (Substitution redundancy). A PB constraint C is redundant with respect to the formula F if and only if there is a substitution ω, called a witness, for which it holds that F C |= (F C) ω .

Proof. ( ) Suppose C is redundant. If F is unsatisﬁable, then for any constraint C it vacuously holds that F |= C . Hence, any substitution ω fulﬁls the condition. If F is satisﬁable, then F C must also be satisﬁable as C is redundant by assumption. If we choose ω to be a satisfying assignment for F C, the implication in the proposition again vacuously holds since (F C) ω is ﬁxed to true. ( ) Suppose now that ω is such that F C |= (F C) ω. If F is unsatisﬁable, then every constraint is redundant and there is nothing to check. Otherwise, let α be a (total) satisfying assignment for F. If α also satisﬁes C, then clearly the constraint is redundant. Now consider the case that α does not satisfy C. If so, α must satisfy C and hence, by the assumed implication, also (F C) ω. But then the assignment β deﬁned by

β(x) = α(x) if x dom(ω), ω(x) otherwise, (9)

satisﬁes both C and F (since (F C) β = ((F C) ω) α by construction), so F C is satisﬁable.

We remark that this proof does not make use of that we are operating with a pseudo-Boolean constraint C we only need that the negation C is easy to represent in the same formalism. Thus, the argument generalizes to other types of constraints with this property. Let us return to our example reiﬁcation of the constraint in (7) and show how this can be derived using substitution redundancy. Let us write C8a for the constraint in (8a) and C8b for (8b), where y is fresh with respect to the current formula F. To show that C8b is substitution redundant with respect to F we choose the witness ω = { y 7 1 }, which clearly satisﬁes C8b. Since y does not appear in F we have F ω = F, and so the implication F C8b |= (F C) ω vacuously holds. Showing that C8a is substitution redundant with respect to F C8b is a bit more interesting. For this we choose ω = { y 7 0 }, which satisﬁes C8a and again leaves F unchanged. Thus, the only implication for which we need to do some work is F C8b C8a |= C8b ω. The negation of C8a is

2y x1 x2 x3 1 , (10)

Algorithm 1 Checking substitution redundancy

1: procedure REDUNDANCYCHECK(F, C, ω) 2: C, ω are given in the proof log to be veriﬁed 3: if RUP(F, C) then return pass 4: for D (F C) ω do 5: if (not (D F or C |= D syntactically) 6: and not RUP(F C, D)) then 7: return fail 8: return pass

or, converted to normalized form,

2y + x1 + x2 + x3 4 (11)

using the rewriting rule ℓ= 1 ℓ. Adding the literal axiom y 0 twice to C8a, and using rewriting again to cancel y + y = 1, we obtain

x1 + x2 + x3 2, (12)

which is C8b ω. Hence, C8a syntactically implies C8b ω, and so F C8b C8a |= C8b ω, completing the proof that C8a is redundant with respect to F C8b. So far, we have not discussed how the implications are veriﬁed. Arbitrary implication checks are as hard as determining satisﬁability, and hence a certiﬁcate that the implication is correct is necessary for efﬁcient veriﬁcation. One way of providing a certiﬁcate could be to exhibit a cutting planes derivation establishing the validity of the implication, as in the example just presented. A more convenient alternative from a proof logging point of view is to follow the lead of DRAT and only allow constraints for which the implication can be veriﬁed using unit propagation. We describe our pseudo-Boolean version of this method in Algorithm 1. This algorithm is very similar to what is used for checking DRAT, except that our unit propagation is on PB constraints rather than clauses and that we need an extra syntactic check on line 5. To see why this check is necessary, note that only unit propagation would fail to certify the correctness of our example above. Assuming for simplicity that F = , if we try to verify C8b C8a |= C8b ω by reverse unit propagation we get the constraints

2y + x1 + x2 + x3 2 [C8b in (8b)] (13a) 2y + x1 + x2 + x3 4 [ C8a in (11)] (13b) x1 + x2 + x3 2 [ (C8b ω)] (13c)

and although visual inspection shows that this collection of constraints is inconsistent, since it requires a majority of the variables { x1, x2, x3 } to be true and false at the same time, unit propagation is too myopic to see this contradiction and only yields y 7 1. Using Algorithm 1, however, allows us to introduce extension variables encoding reiﬁcations y C, which is straightforward to prove by carrying out the same argument as in our example above but for (6a) and (6b) instead of (8a) and (8b). Proposition 2. Let F be a PB formula and C be a PB constraint, and y is a fresh variable that does not appear in F or C. Then the constraints (6a) and (6b) encoding y C can be added to F and checked as redundant by Algorithm 1.

4 Proof Logging for XOR Constraints An XOR or parity constraint, i.e., an equality modulo 2, over k variables is written as x1 x2 xk = b (14) where b { 0, 1 }. Note that we can assume that there is no parity constraint with a negated variable x, because we can always substitute x = x 1. Systems of XOR constraints can arise in a solver during Gaussian elimination (Soos, Nohl, and Castelluccia 2009; Han and Jiang 2012; Laitinen, Junttila, and Niemel a 2012) or conﬂict analysis (Laitinen, Junttila, and Niemel a 2012). To provide proof logging for these approaches we need four ingredients: 1. An efﬁcient encoding of XORs to pseudo-Boolean constraints. 2. A way to derive that encoding for a new XOR constraint from the encodings of existing XORs. 3. A method to translate to this efﬁcient encoding from CNF (which is where we will need to go beyond cutting planes by using extension variables). 4. The ability to provide so-called reason clauses from the PB encoding that can be used by a SAT solver during conﬂict analysis. In the example in Section 5, we will see how these ingredients come together for propagations from parity constraints. It was observed by (Dixon, Ginsberg, and Parkes 2004) that XOR constraints can be encoded and refuted efﬁciently in pseudo-Boolean form by rewriting (14) as P i [k]xi = b + P i [ k/2 ]2yi (15)

for fresh variables yi (where we recall that equality (2a) is a shorthand for (2b) and (2c)). Since the variables yi are otherwise unconstrained, the right-hand side can take any even (odd) value for b = 0 (b = 1) in the range from 0 to k, which are exactly the values that we want to allow for P i [k] xi. In fact, we can generalize this by observing that if we let B denote any integer linear combination of variables, possibly also with a constant term, then the two inequalities P i [k]xi b + 2B (16a) P i [k] xi b 2B , (16b)

forming the equality P i [k] xi = b + 2B, imply the parity

x1 x2 xk = b . (16c) We will make repeated use of this observation below.

XOR Reasoning Whenever we want to combine two XOR constraints to derive a new XOR constraint, as is done during Gaussian elimination, we only need to add the equalities that imply it. For example, suppose that we want to do the derivation x1 x2 x3 = 1 x2 x3 x4 = 1 x1 x4 = 0 (17)

and assume the XORs are represented in pseudo-Boolean form as x1 +x2 +x3 = 2y1 +1 and x2 +x3 +x4 = 2y2 +1. Then adding both equalities together we obtain x1 + 2x2 + 2x3 + x4 = 2y1 + 2y2 + 2, which implies the desired XOR by the observation we just made above for (16c).

Reason Generation Modern SAT solvers built on conﬂict-driven clause learning (CDCL) (Bayardo Jr. and Schrag 1997; Marques-Silva and Sakallah 1999; Moskewicz et al. 2001) operate with clauses. If we want to use XOR constraints to propagate forced variable assignments or derive contradiction, then we need to provide reason clauses that justify such derivation steps. We next show how to derive such reason clauses from pseudo Boolean encodings of XOR constraints. Suppose we have a parity constraint encoded by inequalities of the form (16a) and (16b), and let ρ be an assignment to the k variables xi that is inconsistent with (16a) and (16b), because it falsiﬁes the implied XOR (16c). We want to derive a clause that is falsiﬁed under ρ. Let T be the variables that are set to true under ρ, and F the variables set to false. Using literal axioms we can derive (the normalized form of) the trivially true constraint P x Fx + P x T x |T | , (18)

which when added to (16a), yields P x F2x b |T | + 2B . (19)

Observe that b |T | is always odd, as otherwise ρ would not falsify the XOR implied by (16a) and (16b), while everything else is divisible by 2. Hence we can divide by 2, and rounding up will increase the degree. If we now multiply by 2 again, then we get P x F2x b |T | + 1 + 2B . (20)

We continue by adding (16b) to get P x Fx P x T x 1 |T | , (21)

which is equivalent to the normalized constraint P x Fx + P x T x 1 . (22)

This constraint, which is a disjunctive clause, is falsiﬁed under ρ as desired, and is the reason clause that we need to give to the solver to show why the assignment ρ is inconsistent.

Translating to the Pseudo-Boolean XOR Encoding An XOR as in (14) can be encoded into CNF by having a clause for each of the 2k 1 assignments that falsify the constraint. For example, for k = 3 and b = 1 we get the clauses

x1 + x2 + x3 1 (23a) x1 + x2 + x3 1 (23b) x1 + x2 + x3 1 (23c) x1 + x2 + x3 1 (23d)

(in pseudo-Boolean form). Since the number of clauses in this canonical CNF encoding of an XOR constraint scales exponentially with the number of variables, it is only feasible to encode short XORs into CNF in this way. However, it is possible to split up a long XOR into multiple constantsize XORs using auxiliary variables zi. For example, (14) can be represented as x1 x2 z2 = 0, z2 x3 z3 = 0, . . . , zk 2 xk 1 xk = b. If a parity constraint is split

(a) A 1-bit full adder. (b) Chain of 1-bit full adders.

Figure 1: The output of 1-bit full adders is used to encode new auxiliary Boolean variables, which represent the sum of all Boolean input variables.

up in this way, we only need to re-encode these small parity constraints from CNF into the pseudo-Boolean encoding. Deriving the original long XOR constraint can then be done by XOR reasoning as described earlier. The translation to the pseudo-Boolean XOR encoding from CNF is done in two steps. The ﬁrst step is to derive the constraint P i [k]xi = P i [ k/2 ]2yi + y , (24)

where yi and y are all fresh variables. Note that adding (24) to any formula does not change satisﬁability because we can always assign the fresh variables so that the equality holds. Although the constraint is redundant, we cannot use Proposition 1 directly, because we can not construct a witness assignment ω that is independent of the existing xi variables, and if ω contains any existing variables then the redundancy check in Algorithm 1 may not be strong enough in general. Instead we introduce each fresh variable individually, analogously to what was done in Section 3. The second step is to brute-force all possible assignments for the variables xi, which together with the CNF encoding of the XOR allows us to derive y = b, meaning that we have a constraint of the desired form (24). We remark that this brute-force step is polynomial in the number of clauses of the CNF encoding. We now describe this process in detail. Step 1a. To derive (24) we will construct a chain of 1-bit full adders (see Figure 1b). But let us start ﬁrst by showing how the encoding of a single 1-bit full adder can be derived. A 1-bit full adder (Figure 1a) computes the sum of three variables x1 to x3 and returns the result as a binary number. This can be encoded using the pseudo-Boolean equality

2y + z = x1 + x2 + x3. (25)

To obtain (25) we start by deriving the reiﬁcations

y x1 + x2 + x3 2 (26a) z x1 + x2 + x3 2y 1, (26b)

for fresh variables y and z using substitution redundancy as described in Proposition 2. Writing the constraints in normalized form yields

x1 + x2 + x3 + 2y 2 (27a) x1 + x2 + x3 + 2y 2 (27b) x1 + x2 + x3 + 2y + 3z 3 (27c) x1 + x2 + x3 + 2y + 3z 3. (27d)

To derive the less-than-or-equal part of (25), which in normalized form is

x1 + x2 + x3 + 2y + z 3 , (28)

we add Equation (27c) and 2 times Equation (27a) followed by division by 3. In a similar fashion, to derive the greaterthan-or-equal part of (25), which in normalized form is

x1 + x2 + x3 + 2y + z 3 , (29)

we add Equation (27d) and 2 times Equation (27b) followed by division by 3. Step 1b. To derive Equation (24) we use a chain of 1-bit full adders (Figure 1b). The xi variables are used as input and x2k+1, which is used in the topmost adder, will only occur if the number of variables is odd, otherwise the topmost adder will only have x2k and x2k 1 as input. The variables yi, y encode the sum of the input variables as required for Equation (24). The zi variables are intermediate parity bits. For the topmost adder in Figure 1b we thus have

2yk + zk = x2k+1 + x2k + x2k 1 , (30)

for the intermediate adders we have, for i { 2, . . . , k 1 },

2yi + zi = zi+1 + x2i + x2i 1 , (31)

and for the bottom adder we have

2y1 + y = z2 + x2 + x1 . (32)

By adding the encoding of all 1-bit adders, i.e., Equations (30) to (32), we obtain

i=1 2yi + y +

i=1 xi . (33)

Note that Pk i=2 zi appears on both sides of the equation and hence Equation (33) is equivalent to Equation (24). Indeed, we do not need to remove Pk i=2 zi explicitly during proof logging because it will disappear automatically due to constraint normalization. Step 2. The ﬁnal step is to obtain the value of y by brute-forcing all values of xi. Consider an assignment ρ with ρ(y ) = 1 b that additionally assigns all variables xi and no other variables. Note that there are 2k such assignments. Either ρ falsiﬁes one of the clauses that encode the XOR, or else P i [k] ρ(xi) mod 2 = b = ρ(y ), meaning that Equation (33) is falsiﬁed so that we can derive a clause falsiﬁed

under ρ as described above in our discussion of reason generation. Combining these 2k clauses together we can obtain a clause that forces y to take value b, which we can add to Equation (33) to replace y with a constant value. This concludes the derivation of the pseudo-Boolean encoding (15) of the XOR constraint from a CNF encoding.

5 A Worked-Out Proof Logging Example Consider the two parity constraints x1 x2 x3 = 0 and x2 x3 x4 = 1, which are encoded as clauses by writing

* #variable= 4 #constraint= 8 +1 ~x1 +1 x2 +1 x3 >= 1 ; +1 x1 +1 ~x2 +1 x3 >= 1 ; +1 x1 +1 x2 +1 ~x3 >= 1 ; +1 ~x1 +1 ~x2 +1 ~x3 >= 1 ; +1 x2 +1 x3 +1 x4 >= 1 ; +1 x2 +1 ~x3 +1 ~x4 >= 1 ; +1 ~x2 +1 x3 +1 ~x4 >= 1 ; +1 ~x2 +1 ~x3 +1 x4 >= 1 ;

using the standard OPB ﬁle format1. The solver reads this formula and runs an algorithm to detect clausal encodings of parities. Once a parity is detected, a proof is generated that translates the parity from the clausal encoding into the PB encoding. For this translation it is necessary to introduce fresh variables via substitution redundancy. The proof log contains a line of the form

red [constraint C] ; [assignment omega]

where red identiﬁes the line as a substitution redundancy step, followed by the constraint C to be added and the witness substitution ω, where each variable to be substituted is listed followed by its substitution. A variable and its substitution can optionally be separated by -> . The translation from clausal to PB encoding starts with the reiﬁcation y1 x1 + x2 + x3 2 for the fresh variable y1. In the proof format this is done by the two lines

red 1 x1 1 x2 1 x3 2 ~y1 >= 2 ; y1 -> 0 red 1 ~x1 1 ~x2 1 ~x3 2 y1 >= 2 ; y1 -> 1

which can be checked using Algorithm 1 as discussed in Section 3. After the check passes, the veriﬁer adds these two new constraints to the database and assigns them ids 9 and 10 (the ids 1 to 8 are used for the constraints from the input formula). Similarly, we can do another reiﬁcation y2 x1 + x2 + x3 2y1 1 using the proof lines

red 1 x1 1 x2 1 x3 2 ~y1 3 ~y2 >= 3 ; y2 0 red 1 ~x1 1 ~x2 1 ~x3 2 y1 3 y2 >= 3 ; y2 1

The variables y1, y2 now correspond to the output bits of a single full adder. Because the parity is only over three variables, we do not need to derive a chain of multiple full adders. Note that the constraints arising from reiﬁcation do not need to be added to the database of the solver they are only used for the proof log but the solver should stay clear of using the variables y1, y2 for other purposes. The next step is to combine the constraints we just derived (ids 9 to 12) via a sequence of cutting planes steps, which are

1http://www.cril.univ-artois.fr/PB16/format.pdf

written down in reverse polish notation (using the p-rule in Veri PB), also known as postﬁx notation

p 11 9 2 * + 3 d p 12 10 2 * + 3 d

The ﬁrst line starts with the constraint with id 11 and adds two times the constraint with id 9 and then divides by 3 and rounds up. The same operations are done in the second line but with the constraints with ids 12 and 10. The two lines derive the constraints

(ID: 13) x1 + x2 + x3 + 2y1 + y2 3 (34a) (ID: 14) x1 + x2 + x3 + 2y1 + y2 3 , (34b)

which correspond to (24). The constraints in (34a) and (34b) do not correspond to a parity constraint yet, as they can always be satisﬁed by setting the fresh variables y1, y2 to the right value. To get a proper PB encoding of the ﬁrst parity we need to ﬁx the value of y2, which can be done by generating a brute-force proof via p-rules that derives y2 1, which gets id 15 and can be used to remove y2 from (34b). To remove y2 from (34a) we can simply use the literal axiom y2 0 which is obtained by writing the literal y2 in the p-rule. Both steps together can be written as

p 13 y2 + p 14 15 +

deriving the inequalities encoding the ﬁrst parity, namely

(ID: 16) x1 + x2 + x3 + 2y1 2 (35a) (ID: 17) x1 + x2 + x3 + 2y1 3 , (35b)

which correspond to (15). Analogously, we can derive the pseudo-Boolean encoding for the second parity

(ID: 25) x2 + x3 + x4 + 2y3 3 (36a) (ID: 26) x2 + x3 + x4 + 2y3 4 . (36b)

This concludes the proof logging done after detecting parities. Note that the detection of parities and the proof generation for translating from clausal to PB encoding is only done once in our implementation at the start of the solver. Let us now assume that the solver decides x1 = 0. Note that adding the two parities of the formula yields x1 x4 = 1, and hence x4 should propagate to 1, which is detected by the XOR propagator via Gaussian elimination. The proof for this step is to perform the same addition of the parities, but on their PB representations

p 16 25 + p 17 26 +

which yields new constraints

(ID: 27) x1 + 2x2 + 2x3 + x4 + 2y1 + 2y3 5 (37a) (ID: 28) x1 + 2x2 + 2x3 + x4 + 2y1 + 2y3 7. (37b)

These two constraints imply the parity x1 x4 = 1 by the observation made in connection with (16a) (16c). The reason clause x1 + x4 1 provided by the XOR propagator must be derived in the proof. The assignment falsifying the reason clause is ρ = { x1 7 0, x4 7 0 }. Following the approach in (18) (22), we derive x1 + x4 0 and combine it with the constraints representing the parity

Instance Mini Sat + XOR PR2DRAT (PBP) (DRAT) Urquhart-s5-b1 76.8 3033.1 3878.4 Urquhart-s5-b2 79.8 2844.4 3575.2 Urquhart-s5-b3 116.9 7584.0 7521.0 Urquhart-s5-b4 94.7 5058.6 5271.5

Table 1: Proof sizes (Ki B) for previous Tseitin formulas.

p 27 x1 x4 + + 2 d 2 * 28 +

which derives the constraint x1 + x4 1 as desired. The solver can continue using this clause in the same way as any other clause in its database. These steps for XOR reasoning and reason generation are repeated for every propagation.

6 Implementation and Evaluation As just illustrated in Section 5, we have added a rule to Veri PB2 and its pseudo-Boolean proof format (PBP) to support redundancy checks as described in Algorithm 1, and have implemented our proof logging approach for XOR reasoning in a library together with an XOR engine using Gaussian elimination mod 2 to detect XOR propagations.3 We integrated this library into Mini Sat to call the XOR propagation method every time propagation reached ﬁx point. If the library detects a propagation or conﬂict a callback is used to notify Mini Sat, but the reason clause is only generated when needed in conﬂict analysis. This lazy reason generation technique (Soos, Gocht, and Meel 2020) is crucial, since it avoids generating proofs for reasons that are not used. For comparison, our library also provides DRAT proof logging for XORs as described in (Philipp and Rebola-Pardo 2016). Importantly, our goal was not to investigate whether XOR reasoning is useful this is already known but to provide efﬁcient proof logging for such reasoning. Therefore, we focused on SAT competition benchmarks from the last 5 years that could be solved by Mini Sat with our XOR propagator but not by Kissat, the winner of the 2020 SAT competition. There were 39 such instances, and they could be solved in 0.03 seconds on average by Mini Sat with the XOR propagator. With our new proof logging the average running time increased to 0.05 seconds and unsatisﬁability could be veriﬁed in 1.71 seconds on average. For DRAT proof logging, on the other hand, the average solving time jumped to 7.72 seconds and veriﬁcation took 3291 seconds on average. In order to get systematic measurements for the performance of our new proof logging technique, we ran experiments on so-called Tseitin formulas, including some that have been studied before in the context of proof logging. Tseitin formulas consist of a large inconsistent set of parity constraints, and can thus be viewed as a worst case for XOR reasoning. To the best of our knowledge, the shortest DRAT proofs4 for these formulas obtained so far are based on hand-crafted so-called propagation redundancy

2https://gitlab.com/miao%5Fresearch/veripb 3https://gitlab.com/miao%5Fresearch/xorengine 4The proofs and instances can be found at https://github.com/ marijnheule/drat2er-proofs

3 10 30 100 Instance Size (Ki B)

Proof Size (Mi B)

Proof Format

Figure 2: Proof sizes for Tseitin formulas.

(PR) proofs which have been translated to DRAT using the tool PR2DRAT (Kiesl, Rebola-Pardo, and Heule 2018). Table 1 shows the disk space required for the proofs of Tseitin formulas in (Kiesl, Rebola-Pardo, and Heule 2018). The pseudo-Boolean proofs obtained by Mini Sat with the XOR propagator are dramatically smaller than the DRAT proofs it produces, and the size of our DRAT proofs are similar to that of the best previously known DRAT proofs. To get a sense of the asymptotic behaviour of the proof logging we generated 50 new, larger Tseitin formulas with up to 500 XORs and up to 1250 variables. In Figure 2 we compare the proof size of the proofs as generated. Notice that both proof logging approaches result in a straight line in the log-log plot, which is a strong indication that both approaches are polynomial. Studying the slopes of the lines yields the estimates that DRAT produces quadratic-size proofs while the proof size of the pseudo-Boolean proof is linear in the size of the formula. In Figure 3 we compare the running time (system time + user time) of solving and producing the proof, as well as time spend for veriﬁcation. It is clear that the larger proof size required for DRAT proofs does not only increase veriﬁcation time, but also causes a clearly increased time overhead during solving. All running times were measured on an Intel Core i3-7100U CPU @ 2.40GHz 2 with a memory limit of 8GB, disk write speed of 154 MB/s and read speed of 518 MB/s. The used tools, benchmarks, data and evaluation scripts are available at https://doi.org/10.5281/zenodo.4569840.

7 Conclusion In this work, we present an efﬁcient method for proof logging parity reasoning in conﬂict-driven clause learning (CDCL) solvers, which has been a long-standing challenge in SAT solving. Our method circumvents the prohibitive overhead of current DRAT-based methods by instead using pseudo-Boolean inequalities with extension variables. An experimental evaluation shows that this makes the proof logging overhead, the size of the proof, and the time required for veriﬁcation all go down by an order of magnitude or more compared to DRAT. While there is certainly ample

3 10 30 100 Instance Size (Ki B)

DRAT trim (DRAT verification)

Veri PB (PBP verification)

Mini SAT+XOR (PBP)

Mini SAT+XOR (DRAT)

Figure 3: Solving and veriﬁcation time for Tseitin formulas.

room for further improvements, our ﬁrst proof-of-concept implementation already shows the power of this approach. It is clear that the same method can also be used to solve another task that has remained very challenging for DRAT, namely efﬁcient proof logging for cardinality detection and reasoning. We have not investigated this in this paper, since this is mostly an engineering issue rather than a research problem, given the methods that have already been developed in (Biere et al. 2014; Elffers and Nordstr om 2020). Dealing with symmetries appears to be much more challenging, but our method can do at least as well as (Heule, Hunt Jr., and Wetzler 2015) since it is a strict generalization of DRAT. We would therefore propose that the current extension of the Veri PB method in (Elffers et al. 2020) should be an allowed proof logging format in the SAT competitions. This would make it possible for solvers making use of these advanced techniques to take part in the main track of the SAT competitions, where proof logging is mandatory. However, we believe that the potential beneﬁt of PB proof logging with extension variables goes well beyond the SAT competitions. The original Veri PB method is capable of efﬁcient justiﬁcation of important constraint programming techniques (Elffers et al. 2020), and can also provide proof logging for a wide range of graph problem solvers (Gocht, Mc Creesh, and Nordstr om 2020; Gocht et al. 2020). The pseudo-Boolean rules for reasoning with 0-1 linear constraints provide a simple yet very expressive formalism, and it does not seem out of the question to hope that they could be extended to deal with mixed integer programming (MIP). Thus, we believe that the ultimate goal of this line of research should be to design a uniﬁed proof logging approach for as wide as possible a range of combinatorial optimization paradigms. In addition to furnishing efﬁcient machineveriﬁable proofs of correctness, proof logging could also serve as a valuable tool for debugging and empirical performance analysis during solver development. Furthermore, the proofs produced could in principle provide auditability by third parties using independently developed software, and/or be a stepping stone towards explainability by showing, e.g., why certain solutions are optimal.

Acknowledgments We want to thank Mate Soos and Kuldeep Meel for helpful discussions on how to implement Gaussian elimination modulo 2. The authors were supported by the Swedish Research Council grant 2016-00782, and Jakob Nordstr om also received funding from the Independent Research Fund Denmark grant 9040-00389B.

References Akg un, O.; Gent, I. P.; Jefferson, C.; Miguel, I.; and Nightingale, P. 2018. Metamorphic Testing of Constraint Solvers. In Proceedings of the 24th International Conference on Principles and Practice of Constraint Programming (CP 18), volume 11008 of LNCS, 727 736. Springer. Allouche, D.; Andr e, I.; Barbe, S.; Davies, J.; Givry, S. d.; Katsirelos, G.; O Sullivan, B.; Prestwich, S.; Schiex, T.; and Traor e, S. 2014. Computational Protein Design as an Optimization Problem. Artiﬁcial Intelligence 212(1): 59 79. Archibald, B.; Dunlop, F.; Hoffmann, R.; Mc Creesh, C.; Prosser, P.; and Trimble, J. 2019. Sequential and Parallel Solution-Biased Search for Subgraph Algorithms. In Proceedings of the 16th International Conference on the Integration of Constraint Programming, Artiﬁcial Intelligence, and Operations Research (CPAIOR 19), volume 11494 of LNCS, 20 38. Springer. Bayardo Jr., R. J.; and Schrag, R. 1997. Using CSP Look Back Techniques to Solve Real-World SAT Instances. In Proceedings of the 14th National Conference on Artiﬁcial Intelligence (AAAI 97), 203 208. Biere, A. 2006. Trace Check. http://fmv.jku.at/tracecheck/. Accessed on 2021 03 19. Biere, A.; Le Berre, D.; Lonca, E.; and Manthey, N. 2014. Detecting Cardinality Constraints in CNF. In Proceedings of the 17th International Conference on Theory and Applications of Satisﬁability Testing (SAT 14), volume 8561 of LNCS, 285 301. Springer. Buss, S. R.; and Nordstr om, J. 2021. Proof Complexity and SAT Solving. In Biere, A.; Heule, M. J. H.; van Maaren, H.; and Walsh, T., eds., Handbook of Satisﬁability, volume 336 of Frontiers in Artiﬁcial Intelligence and Applications, chapter 7, 233 350. IOS Press, 2nd edition. Buss, S. R.; and Thapen, N. 2019. DRAT Proofs, Propagation Redundancy, and Extended Resolution. In Proceedings of the 22nd International Conference on Theory and Applications of Satisﬁability Testing (SAT 19), volume 11628 of LNCS, 71 89. Springer. Cook, W.; Coullard, C. R.; and Tur an, G. 1987. On the Complexity of Cutting-Plane Proofs. Discrete Applied Mathematics 18(1): 25 38. Cook, W.; Koch, T.; Steffy, D. E.; and Wolter, K. 2013. A Hybrid Branch-and-Bound Approach for Exact Rational Mixed-Integer Programming. Mathematical Programming Computation 5(3): 305 344. Cruz-Filipe, L.; Heule, M. J. H.; Hunt, W. A.; Kaufmann, M.; and Schneider-Kamp, P. 2017. Efﬁcient Certiﬁed RAT

Veriﬁcation. In Proceedings of the 26th International Conference on Automated Deduction (CADE-26), volume 10395 of LNCS, 220 236. Springer. Cruz-Filipe, L.; Marques-Silva, J.; and Schneider-Kamp, P. 2017. Efﬁcient Certiﬁed Resolution Proof Checking. In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 17), volume 10205 of LNCS, 118 135. Springer. Delorme, M.; Garc ıa, S.; Gondzioa, J.; Kalcsics, J.; Manlove, D.; and Pettersson, W. 2019. Mathematical Models for Stable Matching Problems with Ties and Incomplete Lists. European Journal of Operational Research 277(2): 426 441. Dixon, H. E.; Ginsberg, M. L.; and Parkes, A. J. 2004. Generalizing Boolean Satisﬁability I: Background and Survey of Existing Work. Journal of Artiﬁcial Intelligence Research 21: 193 243. E en, N.; and S orensson, N. 2004. An Extensible SAT-solver. In 6th International Conference on Theory and Applications of Satisﬁability Testing (SAT 03), Selected Revised Papers, volume 2919 of LNCS, 502 518. Springer. Elffers, J.; Gocht, S.; Mc Creesh, C.; and Nordstr om, J. 2020. Justifying All Differences Using Pseudo-Boolean Reasoning. In Proceedings of the 34th AAAI Conference on Artiﬁcial Intelligence (AAAI 20), 1486 1494. Elffers, J.; and Nordstr om, J. 2018. Divide and Conquer: Towards Faster Pseudo-Boolean Solving. In Proceedings of the 27th International Joint Conference on Artiﬁcial Intelligence (IJCAI 18), 1291 1299. Elffers, J.; and Nordstr om, J. 2020. A Cardinal Improvement to Pseudo-Boolean Solving. In Proceedings of the 34th AAAI Conference on Artiﬁcial Intelligence (AAAI 20), 1495 1503. Gange, G.; and Stuckey, P. 2019. Certifying Optimality in Constraint Programming. Presentation at KTH Royal Institute of Technology. Slides available at https://www.kth.se/ polopoly fs/1.879851.1550484700!/Certiﬁed CP.pdf. Gillard, X.; Schaus, P.; and Deville, Y. 2019. Solver Check: Declarative Testing of Constraints. In Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming (CP 19), volume 11802 of LNCS, 565 582. Springer. Gocht, S.; Mc Bride, R.; Mc Creesh, C.; Nordstr om, J.; Prosser, P.; and Trimble, J. 2020. Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP 20), volume 12333 of LNCS, 338 357. Springer. Gocht, S.; Mc Creesh, C.; and Nordstr om, J. 2020. Subgraph Isomorphism Meets Cutting Planes: Solving With Certiﬁed Solutions. In Proceedings of the 29th International Joint Conference on Artiﬁcial Intelligence (IJCAI 20), 1134 1140. Goldberg, E.; and Novikov, Y. 2003. Veriﬁcation of Proofs of Unsatisﬁability for CNF Formulas. In Proceedings of

the Conference on Design, Automation and Test in Europe (DATE 03), 886 891.

Han, C.; and Jiang, J. R. 2012. When Boolean Satisﬁability Meets Gaussian Elimination in a Simplex Way. In Proceedings of the 24th International Conference on Computer Aided Veriﬁcation, (CAV 12), volume 7358 of LNCS, 410 426. Springer.

Heule, M. J. H.; Hunt Jr., W. A.; and Wetzler, N. 2013a. Trimming While Checking Clausal Proofs. In Proceedings of the 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD 13), 181 188.

Heule, M. J. H.; Hunt Jr., W. A.; and Wetzler, N. 2013b. Verifying Refutations with Extended Resolution. In Proceedings of the 24th International Conference on Automated Deduction (CADE-24), volume 7898 of LNCS, 345 359. Springer.

Heule, M. J. H.; Hunt Jr., W. A.; and Wetzler, N. 2015. Expressing Symmetry Breaking in DRAT Proofs. In Proceedings of the 25th International Conference on Automated Deduction (CADE-25), volume 9195 of LNCS, 591 606. Springer.

Heule, M. J. H.; Kiesl, B.; and Biere, A. 2017. Short Proofs Without New Variables. In Proceedings of the 26th International Conference on Automated Deduction (CADE-26), volume 10395 of LNCS, 130 147. Springer.

Kiesl, B.; Rebola-Pardo, A.; and Heule, M. J. H. 2018. Extended Resolution Simulates DRAT. In Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 18), volume 10900 of LNCS, 516 531. Springer.

Laitinen, T.; Junttila, T.; and Niemel a, I. 2012. Conﬂict Driven XOR-Clause Learning. In Proceedings of the 15th International Conference on Theory and Applications of Satisﬁability Testing (SAT 12), volume 7317 of LNCS, 383 396. Springer.

Laitinen, T.; Junttila, T.; and Niemel a, I. 2012. Extending Clause Learning SAT Solvers with Complete Parity Reasoning. In Proceedings of the IEEE 24th International Conference on Tools with Artiﬁcial Intelligence (ICTAI 12), 65 72.

Le Berre, D.; and Parrain, A. 2010. The Sat4j Library, Release 2.2. Journal on Satisﬁability, Boolean Modeling and Computation 7: 59 64.

Leyton-Brown, K.; Milgrom, P.; and Segal, I. 2017. Economics and Computer Science of a Radio Spectrum Reallocation. Proceedings of the National Academy of Sciences 114(28): 7202 7209.

Manlove, D. F. 2016. Hospitals/Residents Problem. In Kao, M.-Y., ed., Encyclopedia of Algorithms, 926 930. Springer New York.

Manlove, D. F.; Mc Bride, I.; and Trimble, J. 2017. Almoststable Matchings in the Hospitals / Residents Problem with Couples. Constraints 22(1): 50 72.

Manlove, D. F.; and O Malley, G. 2012. Paired and Altruistic Kidney Donation in the UK: Algorithms and Experimentation. In Proceedings of the 11th International Sympo-

sium on Experimental Algorithms (SEA 12), volume 7276 of LNCS, 271 282. Springer. Mann, M.; Will, S.; and Backofen, R. 2008. CPSP-tools Exact and Complete Algorithms for High-Throughput 3D Lattice Protein Studies. BMC Bioinformatics 9: 230:1 230:8. Marques-Silva, J. P.; and Sakallah, K. A. 1999. GRASP: A Search Algorithm for Propositional Satisﬁability. IEEE Transactions on Computers 48(5): 506 521. Preliminary version in ICCAD 96. Mc Connell, R. M.; Mehlhorn, K.; N aher, S.; and Schweitzer, P. 2011. Certifying Algorithms. Computer Science Review 5(2): 119 161. Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; and Malik, S. 2001. Chaff: Engineering an Efﬁcient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC 01), 530 535. Pardalos, P. M.; Du, D.-Z.; and Graham, R. L., eds. 2013. Handbook of Combinatorial Optimization. Springer, 2nd edition. Philipp, T.; and Rebola-Pardo, A. 2016. DRAT Proofs for XOR Reasoning. In Proceedings of the 15th European Conference on Logics in Artiﬁcial Intelligence (JELIA 16), volume 10021 of LNCS, 415 429. Springer. Sinz, C.; and Biere, A. 2006. Extended Resolution Proofs for Conjoining BDDs. In Proceedings of the 1st International Computer Science Symposium in Russia (CSR 06), volume 3967 of LNCS, 600 611. Springer. Soos, M.; Gocht, S.; and Meel, K. S. 2020. Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling. In Proceedings of the 32nd International Conference on Computer Aided Veriﬁcation, (CAV 20), volume 12224 of LNCS, 463 484. Springer. Soos, M.; Nohl, K.; and Castelluccia, C. 2009. Extending SAT Solvers to Cryptographic Problems. In Proceedings of the 12th International Conference on Theory and Applications of Satisﬁability Testing (SAT 09), volume 5584 of LNCS, 244 257. Springer. Veksler, M.; and Strichman, O. 2010. A Proof-Producing CSP Solver. In Proceedings of the 24th AAAI Conference on Artiﬁcial Intelligence (AAAI 10), 204 209. Wetzler, N.; Heule, M. J. H.; and Hunt Jr., W. A. 2014. DRAT-trim: Efﬁcient Checking and Trimming Using Expressive Clausal Proofs. In Proceedings of the 17th International Conference on Theory and Applications of Satisﬁability Testing (SAT 14), volume 8561 of LNCS, 422 429. Springer.