Certified CNF Translations for Pseudo-Boolean Solving (Extended Abstract).

1 Introduction

Boolean satisfiability (SAT) solving has witnessed striking improvements over the last decades, starting with the introduction of conflict-driven clause learning (CDCL) [MarquesSilva and Sakallah, 1999; Moskewicz et al., 2001], and this has led to a wide range of applications to large-scale problems in both academia and industry [Biere et al., 2021]. The conflict-driven paradigm has also been successfully exported to other areas such as maximum satisfiability (MaxSAT), pseudo-Boolean (PB) solving, constraint programming (CP), and mixed integer programming (MIP). As combinatorial solvers are used to attack ever more challenging problems, the question arises whether we can trust the results they produce. Sadly, it is well-documented that state-of-the-art CP and MIP solvers can return incorrect solutions [Akg¨un et al., 2018;

∗This is an abbreviated version of a paper published in the Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT '22).

Cook et al., 2013; Gillard et al., 2019]. For SAT solvers, however, analogous problems [Brummayer et al., 2010] have been successfully addressed by the introduction of proof logging, requiring that solvers should be certifying [McConnell et al., 2011] in the sense that they output machine-verifiable proofs of their claims.

A number of different proof formats have been developed for SAT solving, and since 2013 the SAT competitions require solvers to be certifying, with DRAT [Wetzler et al., 2014] established as the standard format. Such proof logging would be highly desirable also for stronger combinatorial solving paradigms, but while methods such as DRAT are extremely powerful in theory, the limitation to a clausal format makes it hard to capture more advanced forms of reasoning concisely. A more fundamental concern is how these proof logging methods should deal with input that is not presented in conjunctive normal form (CNF). One way to address this problem could be to extend the DRAT format [Baek et al., 2021], but another approach pursued in recent years is to develop stronger proof logging methods based on more expressive formalisms, such as binary decision diagrams [Barnett and Biere, 2021], algebraic reasoning [Kaufmann et al., 2022; Kaufmann and Biere, 2021], pseudo-Boolean reasoning [Elffers et al., 2020; Gocht et al., 2020; Gocht and Nordstr¨om, 2021; Bogaerts et al., 2022], and integer linear programming [Cheung et al., 2017; Eifler and Gleixner, 2021].

In this work, we consider the use of CDCL for pseudoBoolean solving, where the pseudo-Boolean input (i.e., a 0-1 integer linear program) is translated to CNF and passed to a SAT solver, as pioneered in MINISAT+ [E´en and S¨orensson, 2006]. While DRAT proof logging can certify unsatisfiability of the translated formula, it cannot prove correctness of the translation, not only since there is no known method of carrying out PB reasoning efficiently in DRAT (except for constraints with small coefficients [Bryant et al., 2022]), but also, and more fundamentally, because the input is not in CNF.

We demonstrate how to instead use the cutting planes proof system [Cook et al., 1987], enhanced with a rule for introducing extension variables [Gocht and Nordstr¨om, 2021], to show that the CNF formula resulting from the translation can be derived from the original pseudo-Boolean constraints. Since this method is a strict extension of DRAT, we can combine the proof for the translation with the SAT solver DRAT proof log. In this way, we achieve end-to-end verification of the pseudo-Boolean solving process using the proof checker VERIPB [Gocht and Nordstr¨om, 2021; Bogaerts et al., 2022] as illustrated in Figure 1.

One challenge when certifying PB-to-CNF translations is that there are many different ways of encoding pseudoBoolean constraints into CNF (as catalogued in, e.g., [Philipp and Steinke, 2015]), and it is time-consuming (and errorprone) to code up proof logging for every single encoding. However, many of the encodings can be understood as first designing a circuit to evaluate whether the PB constraint is satisfied, and then writing down a CNF formula enforcing the computation of this circuit. An important part of our contribution is that we develop a general proof logging method for a wide class of such circuits. The PB format makes it easy to derive 0-1 linear inequalities describing the circuit computations, and once this has been done the clauses in the CNF translation can simply be obtained by so-called reverse unit propagation (RUP) [Goldberg and Novikov, 2003; Van Gelder, 2008], obviating the need for complicated syntactic proofs. We apply this method to the sequential counter [Sinz, 2005], totalizer [Bailleux and Boufkhad, 2003], generalized totalizer [Joshi et al., 2015] and binary adder network [E´en and S¨orensson, 2006; Warners, 1998] encodings, and report results from an empirical evaluation of the efficiency of proof generation and verification.

This paper is only an abbreviated version of the SAT '22 conference paper [Gocht et al., 2022]. We refer the reader to the SAT '22 conference paper or the upcoming full-length version for all the details omitted below.

2 Example: Sequential Counter Encoding

In the interest of brevity, let us give a concrete example of how to certify CNF translations of cardinality constraints using the sequential counter encoding [Sinz, 2005], introducing the necessary terminology and notation as we go along (and referring the reader to, e.g., [Buss and Nordstr¨om, 2021; Gocht and Nordstr¨om, 2021] for more detailed background).

A literal ℓ over a Boolean variable x is x itself or its negation x, where variables can be assigned values 0 (false) or 1 (true), so that x = 1-x. A pseudo-Boolean (PB) constraint C is a 0-1 linear inequality ∑iaiℓi ≥ A, which, without loss of generality, can be assumed to be in normalized form [Barth, 1995]; i.e., all literals ℓi are over distinct variables and the coefficients ai and the degree (of falsity) A are non-negative integers. We use equality constraints ∑iaiℓi = A as syntactic sugar for the corresponding pair of inequalities. A pseudo-Boolean formula is a conjunction of PB constraints. A cardinality constraint is a PB constraint with all coefficients equal to 1. If the degree is also 1, then the constraint ℓ1 + · · · + ℓk ≥ 1 is equivalent to the (disjunctive) clause ℓ1 ∨ · · · ∨ ℓk, and so a CNF formula is just a special case of a pseudo-Boolean formula.

To convert a cardinality constraint ∑ni=1 ℓi ▷◁ k (where ▷◁ denotes ≥, ≤, or =) to CNF using the sequential counter encoding, one constructs a circuit summing up the input bits one by one, with intermediate variables si,j for i ∈ [n] and j ∈ [i] being true if and only if ∑it=1 ℓt ≥ j holds. The variables si,j can be computed as in Figure 2a by the formula

saying that si,j is true either if the first i - 1 literals add up to j - 1 and the ith literal is true, or if already the first i - 1 literals add up to j. The circuit constructed in this way, shown in Figure 2b, can be partitioned into n blocks, where the ith block computes si,j for j ∈ [i] from the ith input bit ℓi and the variables si-1,j in the previous block. One then obtains the CNF encoding by translating each component in Figure 2a (as described by Equation (1)) to the clausal constraints

for i ∈ [n] and j ∈ [i] (where we write these disjunctive clauses in the pseudo-Boolean form that will be used in our proofs). For all i one sets si,0 = 1, so that constraint (2a) simplifies to ℓi + si,1 ≥ 1 and constraint (2d) is satisfied and disappears. In the same way, si-1,i = 0 simplifies (2c) to ℓi + si,i ≥ 1, and (2b) is satisfied and disappears. Once clauses (2a)-(2d) have been generated for all circuit components, one obtains a greater-than-or-equal-to-k constraint by adding the unit clause sn,k ≥ 1. Analogously, a less-than-orequal-to-k constraint is enforced using the clause sn,k+1 ≥ 1.

Our goal is to produce a cutting planes proof that the resulting CNF formula correctly encodes the original cardinality constraint. Since si,j is true if and only if ∑it=1 ℓt ≥ j holds, for all i ∈ [n] we should be able to deduce

However, the sequential counter circuit computes the variables si,j in the ith block using only the variables si-1,j from the previous block and the literal ℓi, and so if we only reason locally about the ith block what we can derive is the equality

If we look at the variables on wires entering and exiting the ith block of the circuit, we see that Equation (4) specifies that the sum of the inputs is equal to the sum of the outputs. This means that if we traverse the blocks and do a telescoping sum, we can easily derive (3). From this, in turn, it is clear that a constraint on the input variables ∑nj=1 ℓi ▷◁ k implies the same constraint on the output variables, and formally this can be obtained by one final telescoping sum step combining ∑nj=1 ℓi ▷◁ k and ∑nj=1 ℓi = ∑nj=1 sn,j to get

• (a) Logic circuit for single component.

Figure 2: Circuit representation of the sequential counter encoding.

Another important property of the variables si,j is that they do not just take any values satisfying (4), but are orderedsince si,j encodes ∑it=1 ℓt ≥ j, it follows that si,j cannot be true unless also si,j ′ is true for all j ′ < j. This can be expressed by ordering constraints

which are semantically implied by the circuit encoding.

Taking this view of the circuit encoding, the task of certifying the correctness of the CNF translation becomes surprisingly simple. If we can derive the pseudo-Boolean constraints (4)-(6), then it can be verified that the clauses of the sequential counter encoding (i.e., (2a)-(2d) plus sn,k+1 ≥ 1 and/or sn,k ≥ 1) all follow by reverse unit propagation, meaning that the clauses can just be claimed as true with the proof left to the proof checker. This is so since when asserting the clauses to false, the ordering constraints (6) will propagate enough variables si,j for (4) to be falsified.

To see how to obtain the constraints (4)-(6), note that we already discussed above how to derive (5) by a telescoping sum over constraints (4), which is straightforward to do with standard cutting planes rules. To get constraints on the form (4), we can first use the redundance-based strengthening rule in [Gocht and Nordstr¨om, 2021] to derive the reified constraints

(which together can be seen to enforce the equivalence si,j ⇔ ℓi + ∑i-1 j=1 si-1,j ≥ j). If we do this in increasing order for i and j, then si,j is a fresh variable for each new pair of constraints (7a)-(7b), which can be shown to imply that these are valid derivation steps. From the constraints (7a)-(7b) we can then derive (4) and (6) (though these steps are slightly trickier, and we refer to [Gocht et al., 2022] for the details).

The fact that we can perform all the derivations on 0-1 linear inequalities using cutting planes reasoning make the steps very efficient (and quite elegant). Although the final constraints we need to derive to prove the correctness of the CNF translation are all clausal, it turns out to be very helpful to be able to use 0-1 inequalities in intermediate steps.

3 Experimental Evaluation

To evaluate the proof logging methods developed in this paper, we have implemented certified translations to CNF for the sequential counter, totalizer, generalized totalizer, and binary adder network encodings in the tool VERITASPBLIB. This tool takes a pseudo-Boolean formula in OPB format [Roussel and Manquinho, 2016] and returns a CNF translation together with a proof logging certificate. We have employed the verifier VERIPB [Gocht and Nordstr¨om, 2021; Bogaerts et al., 2022] to check the certificate returned by VERITASPBLIB, and have used the SAT solver KISSAT (http: //fmv.jku.at/kissat/) in a lightly modified version outputting DRAT proofs in pseudo-Boolean format, to solve the CNF formula. Finally, we have conjoined the certificates from the CNF translation and the SAT solving and verified the end-toend pipeline with VERIPB.

Our evaluation aimed to answer the following questions:

1. Can we use our end-to-end framework to verify the results of CDCL-based pseudo-Boolean solving, and how efficient is the verification?
2. How long does the verification of the proof take when compared to the translation of the PB formula to CNF?

3.1 End-to-End Solving and Verification

We evaluated VERITASPBLIB on 1,534 formulas from the PB Evaluation 2016. Table 1 shows how VERITASPBLIB can be used to generate a CNF formula that can be solved by KISSAT and verified by VERIPB. For instances with cardinality constraints (Card), we use the sequential counter and totalizer encodings to translate those constraints to CNF. For instances with general PB constraints (PB), our translations use the adder network and generalized totalizer (GTE) encodings. Finally, for instances with both cardinality and general translation PB constraints (Card+PB), we use the sequential counter encoding for cardinality constraints and the adder network encoding for PB constraints, henceforth denoted by Seq+Adder.

Figure 3: Comparison between translation and verification.

The column #CNF shows for how many instances VERITASPBLIB successfully generated the CNF translation, which is almost all. The exceptions are 19 instances using GTE and 2 instances using the Seq+Adder encoding. In those cases, the number of clauses generated is too large and exceeds the resource limits used in our evaluation.

The column #Veri presents for how many instances VERIPB verified the translation certificate from VERITASPBLIB. Except for a few instances for GTE and Seq+Adder yielding large proofs, VERIPB is successful. If the translation check passes, then this guarantees that the CNF encoding does not remove any solutions of the pseudo-Boolean formula. The columns #Solved and #Verified under Solving show how many instances can be solved by KISSAT, and from those, how many can be verified by VERIPB. If a satisfiable formula is verified, then all clauses learned by KISSAT are also valid for the original PB formula, as is the satisfying assignment found, and for an unsatisfiable instance we know that the PB input was also unsatisfiable. We can verify 99% of the solved unsatisfiable instances and 95% of satisfiable instances, which shows the feasibility of our approach.

3.2 Translation and Verification

Turning our focus to the certified translation only, our experiments show that the average overhead in running time for proof logging is a factor of 2-3 for all encodings except GTE, which incurs around a factor 5 in overhead. However, since the translation to CNF is fast for the majority of instances, the additional overhead of proof logging is not an issue.

Figure 3 compares the time for VERITASPBLIB to generate the CNF translation and VERIPB to verify it. The verification overhead is far from negligible, but is not unreasonable. Over all encodings, for 75% of benchmarks verification takes at most 49 times longer than translation, and for 98% of benchmarks at most 100 times longer. While some overhead is natural, since the translation algorithm can just output a claimed proof while the verifier needs to perform the calculations to actually check it, our experiments do show that there is room for further improvements in efficiency both for the verifier and for the proof logging methods.

4 Concluding Remarks

In this work, we develop a general framework for certified translations of linear pseudo-Boolean constraints into CNF using cutting-planes-based proof logging. Since our method is a strict extension of DRAT, the proof for the PB-to-CNF translation can be combined with a SAT solver DRAT proof log to provide, for the first time, end-to-end verification for CDCL-based PB solvers. Our use of cutting planes is not only crucial to deal with the PB input format, but the expressivity of the 0-1 linear constraints also allows us to certify the correctness of the translation to CNF in a concise and elegant way. While there is still room for performance improvements in proof logging and verification, our evaluation shows that this approach is feasible in practice. One bottleneck is that the pseudo-Boolean proof checker VERIPB is comparatively slow at verifying DRAT proofs-this could be addressed by having the SAT solver output LRAT proofs instead.

We wish to stress that we view certified PB-to-CNF translations only as a first step. In the conference version of this paper, we expressed optimism that the techniques we have developed could also be extended to core-guided MaxSAT solving [Fu and Malik, 2006], and such results have very recently been announced in [Berg et al., 2023]. While designing efficient proof logging for other MaxSAT approaches such as implicit hitting sets (IHS) [Davies and Bacchus, 2011] and abstract cores [Berg et al., 2020] seems more challenging, we are hopeful that our work could lead to a unified proof logging method for all of modern MaxSAT solving, and also for pseudo-Boolean optimization using cutting-planes-based reasoning as in [Devriendt et al., 2021a; Devriendt et al., 2021b; Elffers and Nordstr¨om, 2018; Le Berre and Parrain, 2010; Smirnov et al., 2021; Smirnov et al., 2022].

Acknowledgements

The authors wish to acknowledge helpful and stimulating discussions with Bart Bogaerts and Ciaran McCreesh. We are particularly grateful to Bart for sharing the manuscript [Vandesande et al., 2022] using a very elegant reification technique that we wish we would have thought of. We believe it would be worth exploring whether similar ideas could be used in our framework to improve the efficiency of verification.

Stephan Gocht and Jakob Nordstr¨om 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. Ruben Martins was supported by National Science Foundation award CCF-1762363 and an Amazon Research Award, and Andy Oertel was supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.