Practically Feasible Proof Logging for Pseudo-Boolean Optimization

Combinatorial search and optimization is a major success story in computer science, and the dramatic improvements in performance of combinatorial solvers over the last couple of decades allow them to be used for solving large-scale real-world problems in model checking [10], cryptanalysis [54], planning [64], kidney allocation for transplants [11, 12], protein design [2, 44], and many other application domains. But modern solvers are highly complex pieces of software, using sophisticated combinations of intelligent inference algorithms driven by intricate heuristics, and it is well documented that even the most mature state-of-the-art combinatorial solvers sometimes return “solutions” that do not satisfy the constraints, or erroneously claim infeasibility or optimality [1, 14, 20, 37]. Such errors could potentially have serious consequences for applications where correctness is a non-negotiable demand, and in more complex settings, where combinatorial solvers are used to solve subproblems, seemingly innocuous off-by-one mistakes can snowball into huge overall errors.

The Boolean satisfiability (SAT) community has pioneered the concept of certifying solvers as the most successful approach to date to address this problem. Certifying solvers do not only produce an answer, but also use proof logging to generate a machine-verifiable mathematical proof that this answer is correct. Many different SAT proof logging formats such as RUP [43], TraceCheck [9], GRIT [22], and LRAT [21] have been developed, with DRAT [46, 47, 71] established as the de facto standard; for the past decade, proof logging has been compulsory in the main track of the SAT competitions [63].

A big part of the success of SAT proof logging is that it is at the same time very easy to implement and very efficient to check. In the DRAT format, all that is required for proof logging is (essentially) for the solver to print the clauses it learns, meaning that the overhead of proof generation can be kept very small (say, less than 10% of solving time). Yet proof checkers are so fast that the time spent on verifying solver claims is within an order of magnitude of solving time, and can sometimes be made as efficient as solving at the price of adding additional proof details as in LRAT proofs [61]. Many SAT proof formats also come with formally verified proof checking backends [21, 22, 51, 66], meaning that the correctness of the final verdict is guaranteed by state-of-the-art formal verification techniques.

Inspired by the success of SAT proof logging, over the years there have been numerous attempts to develop proof logging in other combinatorial solving communities such as constraint programming [28, 60, 69], mixed integer programming [18, 30], satisfiability modulo theories (SMT) solving [3, 4, 8, 48, 65], model counting [15, 17, 36], and automated planning [33, 34, 58]. However, most of these attempts have run into the problem that it is hard to design simple proof systems that can support the full range of solver reasoning techniques used. And if one instead provides specialized proof rules for different techniques, then proof systems quickly become very complex, making efficient proof checking challenging.

In the last few years, pseudo-Boolean (PB) reasoning with $0$–$1$ linear constraints has emerged as a simple and yet expressive proof logging approach for a wide range of solving paradigms and techniques such as SAT-based optimization (MaxSAT) [5, 6, 49], subgraph solving [38, 39, 40], constraint programming [31, 41, 55, 56, 57], automated planning [27], and dynamic programming [23]. Although having a single, unified proof logging method for a large number of seemingly very different combinatorial paradigms appears quite attractive, the actual performance in terms of proof generation and checking has remained at a proof-of-concept stage, far from what would be required for deployment in production-grade software. It seems fair to say that no combinatorial optimization paradigm has been able to deliver proof logging with the efficiency corresponding to what is available for SAT decision problems.

In this work, we present – to the best of our knowledge, for the first time – highly efficient and practical certified solving for a combinatorial optimization problem, thus going beyond the decision problems considered in SAT solving. Using the pseudo-Boolean proof system VeriPB together with the formally verified backend CakePB, we provide a toolchain for linear pseudo-Boolean optimization with fully formally verified conclusions. We show how to implement proof logging for the state-of-the-art pseudo-Boolean solvers RoundingSat [25, 26, 32] and Sat4j [52], covering the full range of advanced techniques used in these solvers. For the main bottleneck in previous pseudo-Boolean proof logging works, namely proof checking, we can now provide formally verified conclusions within a factor $20$ of the solving time, getting close to the overhead factor of $9$ traditionally required in the SAT competitions – this is orders of magnitude faster than even the unverified proof checking in prior work.

To provide some perspective on why our work is a nontrivial contribution, let us briefly explain how SAT proof logging works and why a similar approach is not possible for pseudo-Boolean solving. The workhorse of SAT proof logging is so-called reverse unit propagation (RUP) [43, 68]. If SAT conflict analysis produces a clause, say, $C\doteq x_1\vee x_2\vee {\overline{x}}_3$, from the current constraint database $𝒞$, then in order to verify the correctness of this derivation it is sufficient to assert the negation $\neg C\doteq {\overline{x}}_1\wedge {\overline{x}}_2\wedge x_3$ and check that so-called unit propagation on the constraint database $𝒞$ leads to contradiction.

The concept of RUP can be generalized to pseudo-Boolean constraints [31], where it means achieving integer bounds consistency, but RUP checks are not sufficient to certify pseudo-Boolean solving. At the risk of getting a bit technical, consider the constraints

and suppose that a pseudo-Boolean solver decides to set $x=0$. Then the constraint $C_1$ propagates $y=z=1$, which leads to a conflict with $C_2$. Division-based pseudo-Boolean conflict analysis now weakens away $u$ and $v$ from $C_1$ to get $2x+2y+2z\ge 3$, divides by $2$ to obtain $x+y+z\ge 2$, and finally multiplies this constraint by $2$ and adds to $C_1$ to learn

It is easy to see that this learned constraint can never be satisfied for $\{0,1\}$-valued variables, and so the solver has derived contradiction and can terminate.

The details of the conflict analysis above are not too important, but the crucial observation is that the learned constraint $C_3$ cannot be verified by RUP, because none of the constraints $C_1$, $C_2$, or $\neg C_3\doteq \overline{u}+\overline{v}\le 2$ causes any unit propagations. A more expensive check would be to compute if the linear programming relaxation of these constraints yields an empty polytope – this would be another way of showing that $C_3$ follows from $C_1$ and $C_2$. But such a check also fails here, since $x=y=z=\frac{1}{2}$ and $u=v=1$ is a fractional solution satisfying $C_1$, $C_2$, and $\neg C_3$. The point of this technical detour is to illustrate that SAT-style RUP proof logging cannot be expected to work for pseudo-Boolean solvers, but instead we have to provide much more explicit, syntactic, information about how solvers infer constraints.

Implementing proof logging for the state-of-the-art solvers RoundingSat and Sat4j presents further challenges. In addition to pseudo-Boolean conflict analysis, which maps very naturally to pseudo-Boolean reasoning steps, RoundingSat uses a number of more advanced techniques for which it is much less obvious how to express the reasoning in terms of pseudo-Boolean proof rules. In other cases, the natural proof logging approach turns out to lead to performance issues, which have to be circumvented by using more complex solutions. Sat4j does not cause as many problems in terms of different reasoning techniques, but has a much larger codebase developed over more than two decades. Adding proof generation to this codebase, and finding all the different places where the solver might, for instance, perform minor simplifications of constraints that do not really change anything in terms of semantics but cause syntactic checks to detect unexplained changes and fail, is highly nontrivial.

Our formally verified proof checking is performed in two stages, as is also commonly done for SAT solving. In the first stage, the unverified checker VeriPB elaborates the proof to a more restrictive format for which no search or propagation is required. This elaborated proof is then checked by the formally verified backend CakePB. We have made significant efforts to identify bottlenecks in proof elaboration and formal checking, and this work is a big part of the explanation for why the whole verified proof checking workflow is now so efficient.

The rest of this paper is organized as follows. After reviewing the basics of pseudo-Boolean reasoning and proof logging in Section 2, we discuss proof logging for advanced solving techniques in Sections 3 and 4. In Section 5 we report on our work on optimizing the proof logging and checking pipeline. We present our experimental evaluation in Section 6 and provide some concluding remarks in Section 7. Some additional technical details regarding our proof logging derivations are provided in Appendices A and B.

We start with a condensed review of pseudo-Boolean reasoning, referring the reader to [13, 42] for more details on VeriPB and to [16] for more on proof systems in general. This is followed by a brief description of the concrete syntax and semantics of VeriPB proofs.

Proof logging for the basic conflict-driven search in the pseudo-Boolean solvers RoundingSat and Sat4j is relatively straightforward, since both solvers use the cutting planes proof system for their conflict analysis. However, RoundingSat is tightly integrated with a linear programming (LP) solver [25], which adds extra complications as explained in this section.

Most aspects of the LP reasoning in RoundingSat can be expressed in terms of (positive) linear combinations of constraints and can therefore be logged directly with pol lines, and Chvátal-Gomory cut generation is the same as cutting planes division. However, mixed-integer rounding (MIR) cuts [53] are not natively supported by the VeriPB proof system, and the cut generation procedure turns inequalities into equalities by introducing non-Boolean integral slack variables, which cannot be directly expressed in the proof system.

As shown in [25], the MIR cut with divisor $d\in {\mathbb{N}}^{+}$ applied to ${\sum }_i{a}_i{\mathrm{\ell }}_i\ge A$ yields

which is in general stronger than the constraint

that we obtain by cutting planes division from ${\sum }_i{a}_i{\mathrm{\ell }}_i\ge A$ with divisor $d$ and then multiplying by $Amodd$, which we call the multiplier of the MIR cut. To see this, note that when , (12) has a smaller coefficient for the literal ${\mathrm{\ell }}_i$ than (13).

We illustrate with an example how MIR cuts are generated in RoundingSat. As input, consider the two constraints

and suppose that the multipliers are ${\lambda }_{14}=1$ and ${\lambda }_{15}=4$, the divisor is $d=5$, and $P=\{x_1,x_4\}$ is the set of variables on which we partially weaken (i.e., add literal axioms to reduce the coefficients to the largest multiple of the divisor $d$). For purposes of computation, we introduce an integral slack variable $s_j\ge 0$ for each constraint $C_j$ to obtain the equalities

We take the linear combination

and continue working on the greater-than-or-equal part of this equality. Partially weakening on $x_1$ and $x_4$ by adding ${\overline{x}}_1\ge 0$ and $3\cdot ({\overline{x}}_4\ge 0)$ yields

Next, we apply a MIR cut with divisor $d=5$ to get the inequality

For later use, we note that the multiplier of this MIR cut is $H=(-3)mod5=2$. To obtain the final cut, we subtract $C_{15}^{\prime }$ to cancel the integral slack variable $s_{15}$, which yields

Our formal VeriPB derivation of the MIR cut (21) is a proof by contradiction starting from the negation of this constraint, which is

We first add ${\lambda }_{14}=1$ times C14, but we postpone adding C15. Intuitively, this is done in order to be able to compensate for the subtraction later. In general, we add ${\lambda }_j{C}_j$ for all $j$ such that ${\lambda }_j\le H$, where $H$ is the multiplier of the MIR cut. This results in the constraint

Next, we partially weaken on the variables in $P$, to reduce their coefficients to the largest smaller multiple of $d-H=3$. In this case, we add ${\overline{x}}_1\ge 0$, which yields

Now we divide by $d-H=3$, add $H=2$ times this to (22), and finally add C15, which yields the sequence of constraints

ending with contradiction, establishing correctness of the cut (21). In general, we add $(d-{\lambda }_j)C_j$ for all $j$ such that ${\lambda }_j>H$. The code fragment

shows how the MIR cut example can be formalized as a valid VeriPB derivation.

In Appendix A, we describe how proof logging for MIR cuts is done in full generality.

RoundingSat solves optimization problems using linear search, core-guided search, or a “hybrid” combination of the two [26]. Proof logging for linear search is straightforward, since the solution-improving constraint added by the solver is what is derived by the soli rule. For core-guided optimization the proof logging is more complicated, but we explain by example below. The overall approach is similar to core-guided optimization in MaxSAT [6], from which the technique has been imported, but the details differ significantly since the solver deals with general pseudo-Boolean constraints rather than clauses. Pseudo-Boolean constraints in the VeriPB code examples of this section are mathematically formatted to improve clarity, which is not correct VeriPB syntax.

Consider a minimization problem with objective function $f_o\doteq x_1+2x_2+3x_3+4x_4+5x_5+6x_6$. We initially have an implicit lower bound $f_o\ge 0$.

We begin by running the solver with an additional assumption that $f_o=0$, equivalently $x_1=\mathrm{\dots }=x_6=0$. We either find a solution, which must be optimal, or our assumption is too strong. In that case the solver finds a conflict, say $3x_2+2x_3+x_4+x_5\ge 4$, which we derive with some proof line

as done for conflict analysis. Such a core constraint shows that the assumptions are inconsistent with the input formula. We then turn the core constraint (33) into a cardinality constraint, also called a cardinality core. The most obvious way to do so is to divide by the largest coefficient in the constraint, but it is possible to obtain stronger cardinality constraints through a more complicated algorithm. All of these algorithms can be logged as a sequence of weakening, saturation, and division steps. In our case, the derivation step

divides by $3$ to get $x_2+x_3+x_4+x_5\ge 2$. We proceed to rewrite the objective using the cardinality core (34). To do so, we introduce two new slack variables $y_3$ and $y_4$ so that we can write $x_2+x_3+x_4+x_5=2+y_3+y_4$. Equivalently, writing ${\mathrm{\Delta }}_1\doteq x_2+x_3+x_4+x_5-(2+y_3+y_4)$, we have ${\mathrm{\Delta }}_1=0$. We log the two sides of this equality using the redundance rule. We first log the at-most constraint ${\mathrm{\Delta }}_1\le 0$ with witness $y_3=y_4=1$ and trivial justification. Then we log the at-least constraint ${\mathrm{\Delta }}_1\ge 0$ in two steps, with witnesses $y_3=0$ and $y_4=0$, and justifications the cardinality core (34) and the previous step (36):

To speed up search we give slack variables the additional meaning that $y_j$ is true if and only if $x_2+x_3+x_4+x_5\ge j$. We do so with an ordering constraint of the form $y_3\ge y_4$, which we derive using the redundance rule and witness swapping $y_3$ and $y_4$:

We then proceed to rewrite the objective to $f_r\doteq f_o-\mathrm{\Delta }$, where $\mathrm{\Delta }\doteq 2{\mathrm{\Delta }}_1$ is the difference between the reformulated and original objectives. The multiplier $2$ is the largest number that keeps all coefficients of $f_r$ positive. The new objective is $f_r\doteq x_1+x_3+2x_4+3x_5+6x_6+2y_3+2y_4+4$, and, because $\mathrm{\Delta }=0$, it is equivalent to the original objective. Furthermore, the new objective contains a constant term $4$, which gives us a lower bound of $4$. We log the global reformulation constraint $\mathrm{\Delta }\ge 0$ as $2$ times (37), then log the objective lower bound $f_o\ge 4$ by first logging the trivial constraint $f_r\ge 4$ and then adding $\mathrm{\Delta }\ge 0$:

At this point we run the solver with assumptions $x_i=y_i=0$ again. Suppose that we now obtain a conflict constraint $x_4+x_5+x_6+y_3\ge 1$, which is already a cardinality core.

We now have ${\mathrm{\Delta }}_2\doteq x_4+x_5+x_6+y_3-(1+z_2+z_3+z_4)$. We introduce at-most, at-least, and ordering constraints:

We rewrite the objective again, with $\mathrm{\Delta }\doteq 2{\mathrm{\Delta }}_1+2{\mathrm{\Delta }}_2$. The new objective is $f_r\doteq x_1+x_3+x_5+4x_6+2y_4+2z_2+2z_3+2z_4+6$. We derive the global reformulation constraint $\mathrm{\Delta }\ge 0$ from the previous global reformulation constraint, and then we log the lower bound $f_o\ge 6$:

We run the solver with assumptions $x_i=y_i=z_i=0$ yet another time. Suppose that these assumptions extend to a solution. We log the solution using soli and obtain the objective upper bound $f_o\le 6$, completing the proof.

Expert readers may note that in practice it is too slow to introduce all the slack variables when we reformulate the objective, and we need to introduce variables lazily instead. This means that when we find the first cardinality core, we only introduce $y_3$. Therefore, we define ${\mathrm{\Delta }}_1^{(1)}\doteq x_2+x_3+x_4+x_5-(2+y_3)$, where the notation ${\mathrm{\Delta }}_i^{(j)}$ refers to the $i$-th cardinality core after $j$ slack variables have been introduced. We log constraints encoding that $y_3$ is true if and only if $x_2+x_3+x_4+x_5\ge 3$ is true. We first log the at-most constraint encoding that $x_2+x_3+x_4+x_5\ge 3$ implies $y_3$

with witness $y_3=1$ and trivial justification, and then the at-least constraint encoding that $y_3$ implies $x_1+x_3+x_4+x_5\ge 3$, or equivalently ${\mathrm{\Delta }}_1^{(1)}\ge 0$,

with witness $y_3=0$ and justification the cardinality core (34).

We rewrite the objective to $f_r\doteq f_o-\mathrm{\Delta }$ with $\mathrm{\Delta }\doteq 2{\mathrm{\Delta }}_1^{(1)}$. Observe that we no longer have $\mathrm{\Delta }=0$ but only $\mathrm{\Delta }\ge 0$, therefore all we can say about the objective is $f_o\le f_r$. Nevertheless, this is enough to derive a lower bound on the objective.

Suppose that our next core constraint is $x_4+x_5+x_6+y_3\ge 1$. We now have ${\mathrm{\Delta }}_2^{(1)}\doteq x_4+x_5+x_6+y_3-(1+z_2)$. We introduce at-most and at-least constraints:

Since $y_3$ appears in this cardinality core and will disappear from the objective, we introduce $y_4$ and extend ${\mathrm{\Delta }}_1^{(1)}$ to ${\mathrm{\Delta }}_1^{(2)}\doteq x_2+x_3+x_4+x_5-(2+y_3+y_4)$. We first log the at-most constraint with witness $y_4=y_3$ and justification the previous at-most constraint (51),

and then the at-least constraint with witness $y_4=0$ and justification the previous at-least constraint (52).

We derive the ordering constraint from previous constraints instead of by redundance, as there might be constraints containing $y_3$ which are not obvious to derive under the witness:

We rewrite the objective to $f_r\doteq f_o-\mathrm{\Delta }$ with $\mathrm{\Delta }\doteq 2{\mathrm{\Delta }}_1^{(2)}+2{\mathrm{\Delta }}_2^{(1)}$. As ${\mathrm{\Delta }}_1^{(1)}$ has been extended to ${\mathrm{\Delta }}_1^{(2)}$, we cannot obtain the new global reformulation constraint from the previous global reformulation constraint, therefore we rederive it from scratch.

Assuming that we next find an optimal solution, we complete the proof analogously to the eager case.

We provide proofs of correctness and some further constructions in Appendix B. Most importantly, we touched on eager and lazy sum encodings, but we also support a third reified encoding. Additionally, if we have upper bounds on the objective, we can use that information to derive unit constraints by hardening, and to derive upper bounds on cores, which in turn can be used to derive stronger at-most constraints and stop extending lazy variables earlier.

In this section, we discuss our work on implementing proof logging in the pseudo-Boolean solvers Sat4j and RoundingSat, and how we have optimized the proof checkers VeriPB and CakePB to get close to the levels of SAT proof logging performance.

We have run experiments on the 397 decision instances and 478 optimization instances in the Pseudo-Boolean Competition 2024 [62] on hardware with i5-1145G7 CPUs, 14GB of available RAM, a 100GB solid state drive as storage, and Rocky Linux 8.10 as operating system. We first ran the solvers without proof logging to establish a baseline, and only kept instances solved within a one-hour time limit. We then ran solvers with proof logging, had VeriPB elaborate the proofs, and fed them to the formally verified checker CakePB. Noise due to very small running times was smoothed by computing all ratios as $(1+x)/(1+y)$.

Sat4j Cutting Planes (Figure 1) solves 199 decision and 123 optimization instances. The worst overhead for proof generation is 51.7%; 95% of the instances have an overhead below 14.2%; and the median is 2.6%. All instances are successfully checked within 6,158s. The worst ratio of checking to solving time is 3.83; 95% of the instances are checked within a factor 1.60, and the median is a factor 0.54, which is even faster than solving.

Sat4j Resolution (Figure 2) solves 243 decision and 123 optimization instances. The worst proof logging overhead is 71%; 95% of the instances have an overhead below 42%; and the median is 9.7%. For 3 instances, VeriPB times out after 10h. The worst ratio of proof checking time compared to solving time is a whopping 338. However, 95% of the instances are checked within a factor 20.9; and the median is a factor 1.33. The main reason for the much larger overheads for checking is that Sat4j Resolution essentially writes SAT-style DRAT proofs using RUP steps without annotations. This means that VeriPB has to perform propagation for every clause learned, but pseudo-Boolean propagation is more expensive than clausal propagation and VeriPB has no special handling of clausal proofs.

RoundingSat (Figure 3) solves 297 decision and 258 optimization instances. The worst proof logging overhead is 46.2%; 95% of the instances have an overhead below 21.1%; and the median is 2.7%. One optimization instance cannot be elaborated by VeriPB because the proofs exceed the 100GB of available disk space. On 3 decision and 4 optimization instances VeriPB runs out of memory, and on a further 1 decision and 1 optimization instance CakePB does. All remaining instances are checked within 11,730s. The worst ratio of checking to solving time is 19.17; 95% of the instances are checked within a factor 9.22; and the median is a factor 1.43. This is arguably quite close to what would be expected of SAT proof logging.

In this work, we present a practically feasible and fully formally verified toolchain based on VeriPB and CakePB for certified pseudo-Boolean solving and optimization. Our work covers the full range of techniques in the state-of-the-art solvers RoundingSat and Sat4j, and so should be eminently possible to adapt to other pseudo-Boolean solvers.

From a solver author perspective, however, a key concern for adoption of proof logging is ease of use. One of the lessons learned from our work is that proof logging for basic constraint simplifications such as removing fixed variables is both common and surprisingly tricky to implement correctly and efficiently. Further investigations are warranted into how such simplifications could be handled more smoothly in the proof system. Also, adding a proof rule for mixed integer rounding (MIR) cuts would greatly simplify the proof logging for solvers that employ MIR cut generation techniques from mixed integer programming.

Regarding VeriPB performance, a substantial amount of time is spent on writing and parsing files. Introducing a binary file format for pseudo-Boolean formulas and proofs would alleviate this issue. Checking reverse unit propagation (RUP) steps is another bottleneck. For Sat4j Resolution the obvious remedy would be to implement RUP with annotations. In general, more sophisticated propagation algorithms [24, 59] would probably be helpful. However, for SAT-like proofs with DRAT-style, non-annotated, RUP steps, implementing a dedicated clausal checker along the lines of [71] inside VeriPB appears to be the best way to get truly efficient proof checking, but this seems like an engineering rather than a research problem.

For verified proof checking with CakePB, working on PB solving has led to several improvements on top of earlier optimizations for subgraph solving [39] and MaxSAT preprocessing [49]. Profiling shows the potential for further efficiency gains in checking strengthening steps and cutting planes derivations. Parallelizing the proof elaboration by VeriPB and checking by CakePB also seems worth exploring, especially since both tools support streaming proof files.

To the best of our knowledge, we present the first certified solving toolchain for an optimization problem beyond SAT with performance approaching that of SAT proof logging tools. We are hopeful that our work could point the way towards practically feasible certified solving also for stronger paradigms such as constraint programming and mixed integer programming.