Keywords

1 Introduction

The development of Boolean satisfiability (SAT) solvers is arguably one of the true success stories of modern computer science—today, SAT solvers are routinely used as core engines in many types of complex automated reasoning systems. One example of this is SAT-based optimization, usually referred to as maximum satisfiability (MaxSAT) solving. The improved performance of SAT solvers, coupled with increasingly sophisticated techniques for using SAT solver calls to reason about optimization problems, have made MaxSAT solvers a powerful tool for tackling real-world NP-hard optimization problems [8].

However, Modern MaxSAT solvers are quite intricate pieces of software, and it has been shown repeatedly in the MaxSAT evaluations [51] that even the best solvers sometimes report incorrect results. This was previously a serious issue also for SAT solvers (see, e.g., [13]), but the SAT community has essentially eliminated this problem by requiring that solvers should be certifying [1, 53], i.e., not only report whether a given formula is satisfiable or unsatisfiable but also produce a machine-verifiable proof that this conclusion is correct. Many different SAT proof formats such as RUP  [33], TraceCheck  [7], GRIT  [17], and LRAT  [16] have been proposed, with DRAT  [35, 36, 74] established as the de facto standard; for the last ten years, proof logging has been compulsory in the (main track of the) SAT competitions [66]. It is all the more striking, then, that until recently no similar developments have been observed in MaxSAT solving.

1.1 Previous Work

A first natural question to ask—since MaxSAT solvers are based on repeated calls to SAT solvers—is why we cannot simply use SAT proof logging also for MaxSAT. The problem is that DRAT can only reason about clauses, whereas MaxSAT solvers argue about costs of solutions and values of objective functions. Translating such claims to clausal form would require an external tool to certify correctness of the translation. Also, such clausal translations incur a significant overhead and do not seem well-adapted for, e.g., counting arguments in MaxSAT.

While there have been several attempts to design proof systems specifically for MaxSAT solving  [11, 23, 39, 45, 57, 58, 63,64,65], none of these have come close to providing a general proof logging solution, because they apply only for very specific algorithm implementations and/or fail to capture the full range of techniques used. Recent papers have instead proposed using pseudo-Boolean proof logging with VeriPB  [9, 32] to certify correctness of so-called solution-improving solvers [72] and core-guided solvers [4]. Although these works demonstrate, for the first time, practical proof logging for modern MaxSAT solving, the methods developed thus far only apply to the core solving process. This ignores the preprocessing phase, where the input formula can undergo major reformulation. State-of-the-art solvers sometimes use stand-alone preprocessor tools, or sometimes integrate preprocessing-style reasoning more tightly within the MaxSAT solver engine, to speed up the search for optimal solutions. Some of these preprocessing techniques are lifted from SAT to MaxSAT, but there are also native MaxSAT preprocessing methods that lack analogies in SAT solving.

1.2 Our Contribution

In this paper, we show, for the first time, how to use pseudo-Boolean proof logging with VeriPB to produce proofs of correctness for a wide range of preprocessing techniques used in modern MaxSAT solvers. VeriPB proof logging has previously been successfully used not only for core MaxSAT search as discussed above, but also for advanced SAT solving techniques (including symmetry breaking) [9, 27, 32], subgraph solving [28,29,30], constraint programming [22, 31, 54, 55], and 0–1 ILP presolving [37], and we add MaxSAT preprocessing to this list.

In order to do so, we extend the VeriPB proof format to include an output section where a reformulated output can be presented, and where the pseudo-Boolean proof establishes that this output formula and the input formula are equioptimal, i.e., have optimal solutions of the same value. We also enhance CakePB  [10, 29]—a verified proof checker for pseudo-Boolean proofs—to handle proofs of reformulation. In this way, we obtain an end-to-end formally verified toolchain for certified preprocessing of MaxSAT instances.

It is worth noting that although preprocessing is also a critical component in SAT solving, we are not aware of any tool for certifying reformulations even for the restricted case of decision problems, i.e., showing that formulas are equisatisfiable—the DRAT format and tools support proofs that satisfiability of an input CNF formula F implies satisfiability of an output CNF formula G but not the converse direction (except in the special case where F is a subset of G). To the best of our knowledge, our work presents the first practical tool for proving (two-way) equisatisfiability or equioptimality of reformulated problems.

We have performed computational experiments running a MaxSAT preprocessor with proof logging and proof checking on benchmarks from the MaxSAT evaluations [51]. Although there is certainly room for improvements in performance, these experiments provide empirical evidence for the feasibility of certified preprocessing for real-world MaxSAT benchmarks.

1.3 Organization of This Paper

After reviewing preliminaries in Sect. 2, we explain our pseudo-Boolean proof logging for MaxSAT preprocessing in Sect. 3, and Sect. 4 discusses verified proof checking. We present results from a computational evaluation in Sect. 5, after which we conclude with a summary and outlook for future work in Sect. 6.

2 Preliminaries

We write \(\ell \) to denote a literal, i.e., a \(\{ 0,1 \}\)-valued Boolean variable \(x\) or its negation \(\overline{x} = 1-x\). A clause \(C=\ell _1 \vee \ldots \vee \ell _k\) is a disjunction of literals, where a unit clause consists of only one literal. A formula in conjunctive normal form (CNF) \(F= C_1 \wedge \ldots \wedge C_m\) is a conjunction of clauses, where we think of clauses and formulas as sets so that there are no repetitions and order is irrelevant.

A pseudo-Boolean (PB) constraint is a 0–1 linear inequality \(\sum _j a_j \ell _j \ge b\), where, when convenient, we can assume all literals \(\ell _j\) to refer to distinct variables and all integers \(a_j\) and b to be positive (so-called normalized form). A pseudo-Boolean formula is a conjunction of such constraints. We identify the clause \(C = \ell _1\vee \dots \vee \ell _k\) with the pseudo-Boolean constraint \(\textsc {PB}(C) = \ell _1 + \dots + \ell _k \ge 1\), so a CNF formula \(F\) is just a special type of PB formula \(\textsc {PB}(F) = \{ \textsc {PB}(C) \mid C \in F\}\).

A (partial) assignment \(\rho \) mapping variables to \(\{ 0,1 \}\), extended to literals by respecting the meaning of negation, satisfies a PB constraint \(\sum _j a_j \ell _j \ge b\) if \(\sum _{\ell _j : \rho (\ell _j) = 1} a_j \ge b\) (assuming normalized form). A PB formula is satisfied by \(\rho \) if all constraints in it are. We also refer to total satisfying assignments \(\rho \) as solutions. In a pseudo-Boolean optimization (PBO) problem we ask for a solution minimizing a given objective function \(O= \sum _j c_j \ell _j + W\), where \(c_j\) and \(W\) are integers and \(W\) represents a trivial lower bound on the minimum cost.

2.1 Pseudo-Boolean Proof Logging Using Cutting Planes

The pseudo-Boolean proof logging in VeriPB is based on the cutting planes proof system [15] with extensions as discussed briefly next. We refer the reader to [14] for and in-depth discussion of cutting planes and to [9, 26, 37, 73] for more detailed information about the VeriPB proof system and format.

A pseudo-Boolean proof maintains two sets of core constraints \(\mathcal {C}\) and derived constraints \(\mathcal {D}\) under which the objective \(O\) should be minimized. At the start of the proof, \(\mathcal {C}\) is initialized to the constraints in the input formula \(F\). Any constraints derived by the rules described below are placed in \(\mathcal {D}\), from where they can later be moved to \(\mathcal {C}\) (but not vice versa). The proof system semantics preserves the invariant that the optimal value of any solution to \(\mathcal {C}\) and to the original input problem \(F\) is the same. New constraints can be derived from \(\mathcal {C}\cup \mathcal {D}\) by performing addition of two constraints or multiplication of a constraint by a positive integer, and literal axioms \(\ell \ge 0\) can be used at any time. Additionally, we can apply division to \(\sum _{j} a_j \ell _j \ge b\) by a positive integer d followed by rounding up to obtain \(\sum _{j} \lceil a_j / d \rceil \ell _j \ge \lceil b / d \rceil \), and saturation to yield \(\sum _j \min \{ a_j, b \} \cdot \ell _j \ge b\) (where we again assume normalized form).

The negation of a constraint \(C = \sum _{j} a_j \ell _j \ge b\) is \( \lnot C = \sum _{j} a_j \ell _j \le b - 1\). For a (partial) assignment \(\rho \) we write \({{C}\!\!\upharpoonright _{\rho }}\) for the restricted constraint obtained by replacing literals in C assigned by \(\rho \) with their values and simplifying. We say that C unit propagates \(\ell \) under \(\rho \) if \({{C}\!\!\upharpoonright _{\rho }}\) cannot be satisfied unless \(\ell \) is assigned to 1. If repeated unit propagation on all constraints in \(\mathcal {C}\cup \mathcal {D}\cup \{ \lnot C \}\), starting with the empty assignment \(\rho = \emptyset \), leads to contradiction in the form of an unsatisfiable constraint, we say that C follows by reverse unit propagation (RUP) from \(\mathcal {C}\cup \mathcal {D}\). Such (efficiently verifiable) RUP steps are allowed in VeriPB proofs as a convenient way to avoid writing out an explicit cutting planes derivation. We use the same notation \({{C}\!\!\upharpoonright _{\omega }}\) to denote the result of applying to C a (partial) substitution \(\omega \), which can map variables not only to \(\{ 0,1 \}\) but also to literals, and extend this notation to sets of constraints by taking unions.

In addition to the above rules, which derive semantically implied constraints, there is a redundance-based strengthening rule, or just redundance rule for short, that can derive non-implied constraints C as long as they do not change the feasibility or optimal value. This can be guaranteed by exhibiting a witness substitution \(\omega \) such that for any total assignment \(\alpha \) satisfying \(\mathcal {C}\cup \mathcal {D}\) but violating C, the composition \(\alpha \circ \omega \) is another total assignment that satisfies \(\mathcal {C}\cup \mathcal {D}\cup \{ C \}\) and yields an objective value that is at least as good. Formally, C can be derived from \(\mathcal {C}\cup \mathcal {D}\) by exhibiting \(\omega \) and subproofs for

$$\begin{aligned} \mathcal {C}\cup \mathcal {D}\cup \{ \lnot C \} \vdash {{(\mathcal {C}\cup \mathcal {D}\cup \{ C \})}\!\!\upharpoonright _{\omega }} \cup \{ O\ge {{O}\!\!\upharpoonright _{\omega }} \} \, ,\end{aligned}$$
(1)

using the previously discussed rules (where the notation \(\mathcal {C}_1 \vdash \mathcal {C}_2\) means that the constraints \(\mathcal {C}_2\) can be derived from the constraints \(\mathcal {C}_1\)).

During preprocessing, constraints in the input formula are often deleted or replaced by other constraints, in which case the proof should establish that these deletions maintain equioptimality. Removing constraints from the derived set \(\mathcal {D}\) is unproblematic, but unrestricted deletion from the core set \(\mathcal {C}\) can clearly introduce spurious better solutions. Therefore, removing C from \(\mathcal {C}\) can only be done by the checked deletion rule, which requires a proof that the redundance rule can be used to rederive C from \(\mathcal {C}\setminus \{ C \}\) (see [9] for a more detailed explanation).

Finally, it turns out to be useful to allow replacing \(O\) by a new objective \(O^\prime \) using an objective function update rule, as long as this does not change the optimal value of the problem. Formally, updating the objective from \(O\) to \(O^\prime \) requires derivations of the two constraints \(O\ge O^\prime \) and \(O^\prime \ge O\) from the core set \(\mathcal {C}\), which shows that any satisfying solution to \(\mathcal {C}\) has the same value for both objectives. More details on this rule can be found in [37].

2.2 Maximum Satisfiability

A WCNF instance of (weighted partial) maximum satisfiability \(\mathcal {F}^W= (F_H, F_S)\) is a conjunction of two CNF formulas \(F_H\) and \(F_S\) with hard and soft clauses, respectively, where soft clauses \(C \in F_S\) have positive weights \(w^C\). A solution \(\rho \) to \(\mathcal {F}^W\) must satisfy \(F_H\) and has value \(\textsc {cost}(F_S, \rho )\) equal to the sum of weights of all soft clauses not satisfied by \(\rho \). The optimum \(\textsc {opt}\bigl (\mathcal {F}^W\bigr )\) of \(\mathcal {F}^W\) is the minimum of \(\textsc {cost}(F_S, \rho )\) over all solutions \(\rho \), or \(\infty \) if no solution exists.

State-of-the-art MaxSAT preprocessors such as MaxPre  [39, 44] take a slightly different objective-centric view [5] of MaxSAT instances \(\mathcal {F}= (F, O)\) as consisting of a CNF formula \(F\) and an objective function \(O= \sum _j c_j \ell _j + W\) to be minimized under assignments \(\rho \) satisfying \(F\). A WCNF MaxSAT instance \(\mathcal {F}^W= (F_H, F_S)\) is converted into objective-centric form \(\textsc {ObjMaxSAT}(\mathcal {F}^W) = (F, O)\) by letting the formula \(F= F_H\cup \{ C \vee b_C \mid C \in F_S,|C| > 1 \}\) of \(\textsc {ObjMaxSAT}(\mathcal {F}^W)\) consist of the hard clauses of \(\mathcal {F}^W\) and the non-unit soft clauses in \(F_S\), each extended with a fresh variable \(b_C\) that does not appear in any other clause. The objective \(O= \sum _{(\overline{\ell }) \in F_S} w^{(\overline{\ell })} \ell + \sum w^C b_C\) contains literals \(\ell \) for all unit soft clauses \(\overline{\ell }\) in \(F_S\) as well as literals for all new variables \(b_C\), with coefficients equal to the weights of the corresponding soft clauses. In other words, each unit soft clause \(\overline{\ell } \in F_S\) of weight \(w\) is transformed into the term \(w\cdot \ell \) in the objective function \(O\), and each non-unit soft clause C is transformed into the hard clause \(C \vee b_C\) paired with the unit soft clause \((\overline{b}_C)\) with same weight as C. The following observation summarizes the properties of \(\textsc {ObjMaxSAT}(\mathcal {F}^W)\) that are central to our work.

Observation 1

For any solution \(\rho \) to a WCNF MaxSAT instance \(\mathcal {F}^W\) there exists a solution \(\rho '\) to \((F, O) = \textsc {ObjMaxSAT}(\mathcal {F}^W)\) with \(O(\rho ') = \textsc {cost}(\mathcal {F}^W, \rho )\). Conversely, if \(\rho '\) is a solution to \(\textsc {ObjMaxSAT}(\mathcal {F}^W)\), then there exists a solution \(\rho \) of \(\mathcal {F}^W\) for which \(\textsc {cost}(\mathcal {F}^W, \rho ) \le O(\rho ')\).

For the second part of the observation, the reason \(O(\rho ')\) is only an upper bound on \(\textsc {cost}(\mathcal {F}^W, \rho )\) is that the encoding forces \(b_C\) to be true whenever C is not satisfied by an assignment but not vice versa.

An objective-centric MaxSAT instance \((F, O)\), in turn, clearly has the same optimum as the pseudo-Boolean optimization problem of minimizing \(O\) subject to \(\textsc {PB}(F)\). For the end-to-end formal verification, the fact that this coincides with \(\textsc {opt}\bigl (\mathcal {F}^W\bigr )\) needs to be formalized into theorems as shown in Fig. 4.

3 Proof Logging for MaxSAT Preprocessing

We now discuss how pseudo-Boolean proof logging can be used to reason about correctness of MaxSAT preprocessing steps. Our approach maintains the invariant that the current working instance in the preprocessor is synchronized with the PB constraints in the core set \(\mathcal {C}\) as described in Sect. 2.2. At the end of each preprocessing step (i.e., application of a preprocessing technique) the set of derived constraints \(\mathcal {D}\) is empty. All constraints derived in the proof as described in this section are moved to the core set, and constraints are always removed by checked deletion from the core set. Full details are in the online appendix [40].

Fig. 1.
figure 1

Overview of the five stages of certified MaxSAT preprocessing of a WCNF instance \(\mathcal {F}^W\). The middle column contains the state of the working MaxSAT instance as a WCNF instance and a lower bound on its optimum cost (Stages 1–2), or as an objective-centric instance (Stages 3–5). The right column contains a tuple \((\mathcal {C}, O)\) with the set \(\mathcal {C}\) of core constraints, and objective \(O\), respectively, of the proof after each stage.

Full size image

3.1 Overview

All our preprocessing steps maintain equioptimality, which means that if preprocessing of the WCNF MaxSAT instance \(\mathcal {F}^W\) yields the output instance \(\mathcal {F}^W_P\), then the equality \(\textsc {opt}\bigl ( \mathcal {F}^W\bigr ) = \textsc {opt}\bigl ( \mathcal {F}^W_P \bigr )\) is guaranteed to hold. Our preprocessing is certified, meaning that we provide a machine-verifiable proof justifying this claimed equality. Our discussion below focuses on input instances that have solutions, but our techniques also handle the—arguably less interesting—case of  \(\mathcal {F}^W\) not having solutions; details are in the online appendix [40].

An overview of the workflow of our certifying MaxSAT preprocessor is shown in Fig. 1. Given a WCNF instance \(\mathcal {F}^W\) as input, the preprocessor proceeds in five stages (illustrated on the left in Fig. 1), and then outputs a preprocessed MaxSAT instance \(\mathcal {F}^W_P\) together with a pseudo-Boolean proof that \( \textsc {opt}\bigl (\textsc {ObjMaxSAT}\bigl (\mathcal {F}^W\bigr )\bigr ) = \textsc {opt}\bigl (\textsc {ObjMaxSAT}\bigl (\mathcal {F}^W_P\bigr )\bigr ) \). For certified MaxSAT preprocessing, this proof can then be fed to a formally verified checker as in Sect. 4 to verify that (a) the initial core constraints in the proof correspond exactly to the clauses in \(\textsc {ObjMaxSAT}\bigl (\mathcal {F}^W\bigr )\), (b) each step in the proof is valid, and (c) the final core constraints in the proof correspond exactly to the clauses in \(\textsc {ObjMaxSAT}\bigl (\mathcal {F}^W_P\bigr )\). Below, we provide more details on the five stages of the preprocessing flow.

Stage 1: Initialization. An input WCNF instance \(\mathcal {F}^W\) is transformed to pseudo-Boolean format by converting it to an objective-centric representation \((F^0, O^0) = \textsc {ObjMaxSAT}\bigl (\mathcal {F}^W\bigr )\) and then representing all clauses in \(F^0\) as pseudo-Boolean constraints as described in Sect. 2.2. The VeriPB proof starts out with core constraints \(\textsc {PB}(F^0)\) and objective \(O^0\). The preprocessor maintains a lower bound on the optimal cost of the working instance, which is initialized to 0 for the input \(\mathcal {F}^W\).

Stage 2: Preprocessing on the Initial WCNF Representation. During preprocessing on the WCNF representation, a (very limited) set of simplification techniques are applied on the working formula. At this stage the preprocessor removes duplicate, tautological, and blocked clauses [43]. Additionally, hard unit clauses are unit propagated and clauses subsumed by hard clauses are removed. Importantly, the preprocessor is performing these simplifications on a WCNF MaxSAT instance where it deals with hard and soft clauses. As the pseudo-Boolean proof has no concept of hard or soft clauses, the reformulation steps must be expressed in terms of the constraints in the proof. The next example illustrates how reasoning with different types of clauses is logged in the proof.

Example 1

Suppose the working instance has two duplicate clauses C and D. If both are hard, then the proof has two identical constraints \(\textsc {PB}(C)\) and \(\textsc {PB}(D)\) in the core set, and \(\textsc {PB}(D)\) can be deleted since it follows from \(\textsc {PB}(C)\) by reverse unit propagation (RUP). If D is instead a non-unit soft clause, the proof has the constraint \(\textsc {PB}(D \vee b_D)\) and the term \(w^D b_D\) in the objective, where \(b_D\) does not appear in any other constraint. Then in the proof we (1) remove the RUP constraint \(\textsc {PB}(D \vee b_D)\), (2) introduce \(\overline{b}_D \ge 1\) by redundance-based strengthening using the witness \(\{b_D \rightarrow 0\}\), (3) remove the term \(w^D b_D\) from the objective, and (4) delete \(\overline{b}_D \ge 1\) with the witness \(\{b_D \rightarrow 0\}\).

Stage 3: Conversion to Objective-Centric Representation. In order to apply more simplification rules in a cost-preserving way, the working instance \(\mathcal {F}^W_1 = (F_H^1, F_S^1)\) at the end of Stage 2 is converted into the corresponding objective-centric representation that takes the lower-bound \(\textsc {lb}\) inferred during Stage 1 into account. More specifically, the preprocessor next converts its working MaxSAT instance into the objective-centric instance \(\mathcal {F}_2 = (F^2, O^2 + \textsc {lb})\) where \((F^2, O^2) = \textsc {ObjMaxSAT}(\mathcal {F}^W_1)\).

Here it is important to note that at the end of Stage 2, the core constraints \(\mathcal {C}^1\) and objective \(O^1\) of the proof are not necessarily \(\textsc {PB}(F^2)\) and \(O^2 + \textsc {lb}\), respectively. Specifically, consider a unit soft clause \((\overline{\ell })\) of \(\mathcal {F}^W_1\) obtained by shrinking a non-unit soft clause \(C \supseteq (\overline{\ell })\) of the input instance, with weight \(w^C\). Then the objective function \(O^2\) in the preprocessor will include the term \(w^{C} \ell \) that does not appear in the objective function \(O^1\) in the proof. Instead, \(O^1\) contains the term \(w^{C} b_{C}\) and \(\mathcal {C}^1\) the constraint \(\overline{\ell } + b_{C} \ge 1\) where \(b_{C}\) is the fresh variable added to C in Stage 1. In order to “sync up” the working instance and the proof we (1) introduce \(\ell + \overline{b}_C \ge 1\) to the proof with the witness \(\{b_C \rightarrow 0\}\), (2) update \(O^1\) by adding \(w^C \ell - w^C b_C\), (3) remove the constraint \(\ell + \overline{b}_C \ge 1\) with the witness \(\{b_C \rightarrow 0\}\), and (4) remove the constraint \(\overline{\ell } +b_C \ge 1\) with witness \(\{b_C \rightarrow 1\}\). The same steps are logged for all soft unit clauses of \(\mathcal {F}^W_1\) obtained during Stage 2. In the following stages, the preprocessor will operate on an objective-centric MaxSAT instance whose clauses correspond exactly to the core constraints of the proof.

Stage 4: Preprocessing on the Objective-Centric Representation. During preprocessing on the objective-centric representation, more simplification techniques are applied to the working objective-centric instance and logged to the proof. We implemented proof logging for a wide range of preprocessing techniques. These include MaxSAT versions of rules commonly used in SAT solving like bounded variable elimination (BVE) [20, 68], bounded variable addition [49], blocked clause elimination [43], subsumption elimination, self-subsuming resolution [20, 60], failed literal elimination [24, 46, 75], and equivalent literal substitution [12, 48, 71]. We also cover MaxSAT-specific preprocessing rules like TrimMaxSAT [61], (group)-subsumed literal (or label) elimination (SLE) [6, 44], intrinsic at-most-ones [38, 39], binary core removal (BCR) [25, 44], label matching [44], and hardening [2, 39, 56]. Here we give examples for BVE, SLE, label matching, and BCR—the rest are detailed in the online appendix [40]. In the following descriptions, let \((F, O)\) be the current objective-centric working instance.

Bounded Variable Elimination (BVE)  [20, 68]. BVE eliminates from \(F\) a variable x that does not appear in the objective by replacing all clauses in which either x or \(\overline{x}\) appears with the non-tautological clauses in \(\{C \vee D\mid C \vee x \in F, D \vee \overline{x} \in F\}\).

An application of BVE is logged as follows: (1) each non-tautological constraint \(\textsc {PB}(C\vee D)\) is added by summing the existing constraints \(\textsc {PB}(C \vee x)\) and \(\textsc {PB}(D \vee \overline{x})\) and saturating, after which (2) each constraint of the form \(\textsc {PB}(C \vee x)\) and \(\textsc {PB}(D \vee \overline{x})\) is deleted with the witness \(x \rightarrow 1\) or \(x \rightarrow 0\), respectively.

Label Matching  [44]. Label matching allows merging pairs of objective variables that can be deduced to not both be set to 1 by optimal solutions. Assume that (i) \(F\) contains the clauses \(C\vee b_C\) and \(D\vee b_D\), (ii) \(b_C\) and \(b_D\) are objective variables with the same coefficient \(w\) in \(O\), and (iii) \(C\vee D\) is a tautology. Then label matching replaces \(b_C\) and \(b_D\) with a fresh variable \(b_{CD}\), i.e., replaces \(C\vee b_C\) and \(D\vee b_D\) with \(C\vee b_{CD}\) and \(D\vee b_{CD}\) and adds \(-wb_C-wb_D+wb_{CD}\) to \(O\).

As \(C \vee D\) is a tautology there is some literal \(\ell \) such that \(\overline{\ell }\in C\) and \(\ell \in D\). Label matching is logged via the following steps: (1) introduce the constraint \(\overline{b}_C + \overline{b}_D \ge 1\) with the witness \(\{b_C\rightarrow \ell , b_D\rightarrow \overline{\ell }\}\), (2) introduce the constraints \(b_{CD} + \overline{b}_C + \overline{b}_D \ge 2\) and \(\overline{b}_{CD} + b_C + b_D \ge 1\) by redundance; these correspond to \(b_{CD} = b_C + b_D\) which holds even though the variables are binary due to the constraint added in the first step, (3) update the objective by adding \(-wb_C-wb_D+wb_{CD}\) to it, (4) introduce the constraints \(\textsc {PB}(C\vee b_{CD})\) and \(\textsc {PB}(D\vee b_{CD})\) which are RUP, (5) delete \(\textsc {PB}(C\vee b_C)\) and \(\textsc {PB}(D\vee b_D)\) with the witness \(\{b_C\rightarrow \overline{\ell }, b_D\rightarrow \ell \}\), (6) delete the constraint \(b_{CD} + \overline{b}_C + \overline{b}_D \ge 2\) with the witness \(\{b_C \rightarrow 0, b_D \rightarrow 0\}\) and \(\overline{b}_{CD} + b_C + b_D \ge 1\) with the witness \(\{b_C \rightarrow 1, b_D \rightarrow 0\}\), (7) delete \(\overline{b}_C + \overline{b}_D \ge 1\) with the witness \(\{b_C \rightarrow 0\}\).

Subsumed Literal Elimination (SLE)  [6, 39]. Given two non-objective variables x and y such that (i) \(\{ C \mid C \in F, y \in C\} \subseteq \{ C \mid C \in F, x \in C\}\) and (ii) \(\{ C \mid C \in F, \overline{x} \in C\} \subseteq \{ C \mid C \in F, \overline{y} \in C\}\), subsumed literal elimination (SLE) allows fixing \(x=1\) and \(y=0\). This is proven by (1) introducing \(x\ge 1\) and \(\overline{y}\ge 1\), both with witness \(\{x\rightarrow 1\), \(y\rightarrow 0\}\), (2) simplifying the constraint database via propagation, and (3) deleting the constraints introduced in the first step as neither x nor y appears in any other constraints after simplification.

If x and y are objective variables, the application of SLE additionally requires that: (iii) the coefficient in the objective of x is at most as high as the coefficient of y. Then the value of x is not fixed as it would incur cost. Instead, only \(y=0\) is fixed and y removed from the objective. Intuitively, conditions (i) and (ii) establish that the values of x and y can always be flipped to 0 and 1, respectively, without falsifying any clauses. If neither of the variables is in the objective, this flip does not increase the cost of any solutions. Otherwise, condition (iii) ensures that the flip does not make the solution worse, i.e., increase its cost.

Binary Core Removal (BCR)  [25, 44]. Assume that the following four prerequisites hold: (i) \(F\) contains a clause \(b_C \vee b_D\) for two objective variables \(b_C\) and \(b_D\), (ii) \(b_C\) and \(b_D\) have the same coefficient w in \(O\), (iii) the negations \(b_C\) and \(b_D\) do not appear in any clause of F, and (iv) both \(b_C\) and \(b_D\) appear in at least one other clause of F but not together in any other clause of F. Binary core removal replaces all clauses containing \(b_C\) or \(b_D\) with the non-tautological clauses in \(\{ C \vee D \vee b_{CD} \mid C \vee b_C\in F, D \vee b_D\in F\}\), where \(b_{CD}\) is a fresh variable, and modifies the objective function by adding \(-w b_C -w b_D +wb_{CD}+w\) to it.

BCR is logged as a combination of the so-called intrinsic at-most-ones technique [38, 39] and BVE. Applying intrinsic at most ones on the variables \(b_C\) and \(b_D\) introduces a new clause \((\overline{b}_C \vee \overline{b}_D \vee b_{CD})\) and adds \(-w b_C - w b_D + w b_{CD} + w\) to the objective. Our proof for intrinsic at most ones is the same as the one presented in [4]. As this step removes \(b_C\) and \(b_D\) from the objective, both can now be eliminated via BVE.

Stage 5: Constant Removal and Output. After objective-centric preprocessing, the final objective-centric instance \((F^3, O^3)\) is converted back to a WCNF instance. Before doing so, the constant term \(W_3\) of \(O^3\) is removed by introducing a fresh variable \(b^{W_3}\), and setting \(F^4 = F^3 \wedge (b^{W_3})\) and \(O^4 = O^3 - W_3 + W_3 b^{W_3}\). This step is straightforward to prove.

Finally, the preprocessor outputs the WCNF instance \(\mathcal {F}^W_P = (F^4, F_S^P)\) that has \(F^4\) as hard clauses. The set \(F_S^P\) of soft clauses consists of a unit soft clause \((\overline{\ell })\) of weight c for each term \(c \cdot \ell \) in \(O^4\). The preprocessor also outputs the final proof of the fact that the minimum-cost of solutions to the pseudo-Boolean formula \(\textsc {PB}(F^0)\) under \(O^0\) is the same as that of \(\textsc {PB}(F^4)\) under \(O^4\), i.e. that \(\textsc {opt}(\textsc {ObjMaxSAT}(\mathcal {F}^W)) = \textsc {opt}(\textsc {ObjMaxSAT}(\mathcal {F}^W_P))\).

3.2 Worked Example of Certified Preprocessing

Table 1. Example proof produced by a certifying preprocessor. The column (ID) refers to constraint IDs in the pseudo-Boolean proof. The column (Step) indexes all proof logging steps and is used when referring to the steps in the discussion. The letter \(\omega \) is used for the witness substitution in redundance-based strengthening steps.
Full size table

We give a worked-out example of certified preprocessing of the instance \(\mathcal {F}^W= (F_H, F_S)\) where \(F_H= \{ (x_1 \vee x_2), (\overline{x}_2)\}\) and three soft clauses: \((\overline{x}_1)\) with weight 1, \((x_3 \vee \overline{x}_4)\) with weight 2, and \( (x_4 \vee \overline{x}_5)\) with weight 3. The proof for one possible execution of the preprocessor on this input instance is detailed in Table 1.

During Stage 1 (Steps 1–4 in Table 1), the core constraints of the proof are initialized to contain the four constraints corresponding to the hard and non-unit soft clauses of \(\mathcal {F}^W\) (IDs (1)–(4) in Table 1), and the objective to \(x_1 + 2b_1 + 3b_2\), where \(b_1\) and \(b_2\) are fresh variables added to the non-unit soft clauses of \(\mathcal {F}^W\).

During Stage 2 (Steps 5–9), the preprocessor fixes \(x_2 = 0\) via unit propagation by removing \(x_2\) from the clause \((x_1 \vee x_2)\), and then removing the unit clause \((\overline{x}_2)\). The justification for fixing \(x_2 = 0\) are Steps 5–7. Next the preprocessor fixes \(x_1=1\) which (i) removes the hard clause \((x_1)\), and (ii) increases the lower bound on the optimal cost by 1. The justification for fixing \(x_1 = 1\) are Steps 8 and 9 of Table 1. At this point—at the end of Stage 2—the working instance \(\mathcal {F}^W_1 = (F_H^1, F_S^1)\) has \(F_H^1 = \{\}\) and \(F_S^1 = \{ (x_3 \vee \overline{x}_4), (x_4 \vee \overline{x}_5)\}\).

In Stage 3, the preprocessor converts its working instance into the objective-centric representation \((F, O)\) where \(F= \{ (x_3 \vee \overline{x}_4 \vee b_1), (x_4 \vee \overline{x}_5 \vee b_2)\}\) and \(O= 2b_1 + 3b_2 + 1\), which exactly matches the core constraints and objective of the proof after Step 9. Thus, in this instance, the conversion does not result in any proof logging steps. Afterwards, during Stage 4 (Steps 10–17), the preprocessor applies BVE in order to eliminate \(x_4\) (Steps 10–12) and SLE to fix \(b_2\) to 0 (Steps 13–17). Finally, Steps 18 and 19 represent Stage 5, i.e., the removal of the constant 1 from the objective. After these steps, the preprocessor outputs the preprocessed instance \(\mathcal {F}^W_P = (F_H^P, F_S^P)\), where \(F_H^P = \{ (x_3 \vee \overline{x}_5 \vee b_1), (b_3)\}\) and \(F_S^P\) contains two clauses: \((\overline{b}_1)\) with weight 2, and \((\overline{b}_3)\) with weight 1.

4 Verified Proof Checking for Preprocessing Proofs

This section presents our new workflow for formally verified, end-to-end proof checking of MaxSAT preprocessing proofs based on pseudo-Boolean reasoning; an overview of this workflow is shown in Fig. 2. To realize this workflow, we extended the VeriPB tool and its proof format to support a new output section for declaring (and checking) reformulation guarantees between input and output PBO instances (Sect. 4.1); we similarly modified CakePB  [29] a verified proof checker to support the updated proof format (Sect. 4.2); finally, we built a verified frontend, CakePBwcnf, which mediates between MaxSAT WCNF instances and PBO instances (Sect. 4.3). Our formalization is carried out in the HOL4 proof assistant [67] using CakeML tools [34, 59, 70] to obtain a verified executable implementation of CakePBwcnf.

Fig. 2.
figure 2

Workflow for end-to-end verified MaxSAT preprocessing proof checking.

Full size image

In the workflow in Fig. 2, the MaxSAT preprocessor produces a reformulated output WCNF together with a proof of equioptimality with the input WCNF. This proof is elaborated by VeriPB and then checked by CakePBwcnf, resulting in a verified verdict—in case of success, the input and output WCNFs are equioptimal. This workflow also supports verified checking of WCNF MaxSAT solving proofs (where the output parts of the flow are omitted).

4.1 Output Section for Pseudo-Boolean Proofs

Given an input PBO instance \((F,O)\), the VeriPB proof system as described in Sect. 2.1 maintains the invariant that the core constraints \(\mathcal {C}\) (and current objective) are equioptimal to the input instance. Utilizing this invariant, the new output section for VeriPB proofs allows users to optionally specify an output PBO instance \((F',O')\) at the end of a proof. This output instance is claimed to be a reformulation of the input which is either: (i) derivable, i.e., satisfiability of \(F\) implies satisfiability of \(F'\), (ii) equisatisfiable to \(F\), or (iii) equioptimal to \((F,O)\). These are increasingly stronger claims about the relationship between the input and output instances. After checking a pseudo-Boolean derivation, VeriPB runs reformulation checking which, e.g., for equioptimality, checks that \(\mathcal {C}\subseteq F'\), \(F' \subseteq \mathcal {C}\), and that the respective objective functions are syntactically equal after normalization; other reformulation guarantees are checked analogously.

The VeriPB tool supports an elaboration mode [29], where in addition to checking the proof it also converts it from augmented format to kernel format. The augmented format contains syntactic sugar rules to facilitate proof logging for solvers and preprocessors like MaxPre, while the kernel format is supported by the formally verified proof checker CakePB. The new output section is passed unchanged from augmented to kernel format during elaboration.

4.2 Verified Proof Checking for Reformulations

There are two main verification tasks involved in extending CakePB with support for the output section. The first task is to verify soundness of all cases of reformulation checking. Formally, the equioptimality of an input PBO instance fml, obj and its output counterpart fml \(^{\prime }\), obj \(^{\prime }\) is specified as follows:

$$\begin{aligned} &\textsf{sem}\_\textsf{output}\;\textit{fml}\;\textit{obj}\;\textsf{None}\;\textit{fml\,}^{\prime {}}\;{\textit{obj\,}^{\prime {}}}\;\textsf{Equioptimal}\;\mathrel {\overset{{\textsf {def}}}{=}}\\ &\;\;{\forall \,}{} \textit{v}.\;({\exists \,}{} \textit{w}.\;\textsf{satisfies}\;\textit{w}\;\textit{fml}\;{\wedge {}}\;\textsf{eval}\_\textsf{obj}\;\textit{obj}\;\textit{w}\;{\le }\;\textit{v})\;{\iff }\\ &\;\;\;\;\;\;\;\;\;({\exists \,}{\textit{w}^{\prime {}}}.\;\textsf{satisfies}\;{\textit{w}^{\prime {}}}\;{\textit{fml\,}^{\prime {}}}\;{\wedge {}}\;\textsf{eval}\_\textsf{obj}\;{\textit{obj\,}^{\prime {}}}\;{\textit{w}^{\prime {}}}\;{\le }\;\textit{v}) \end{aligned}$$

This definition says that, for all values v, the input instance has a satisfying assignment with objective value less than or equal to v iff the output instance also has such an assignment; note that this implies (as a special case) that fml is satisfiable iff fml’ is satisfiable. The verified correctness theorem for CakePB says that if CakePB successfully checks a pseudo-Boolean proof in kernel format and prints a verdict declaring equioptimality, then the input and output instances are indeed equioptimal as defined in sem_output.

The second task is to develop verified optimizations to speedup proof steps which occur frequently in preprocessing proofs; some code hotspots were also identified by profiling the proof checker against proofs generated by MaxPre. Similar (unverified) versions of these optimizations are also used in VeriPB. These optimizations turned out to be necessary in practice—they mostly target steps which, when naïvely implemented, have quadratic (or worse) time complexity in the size of the constraint database.

Optimizing Reformulation Checking. The most expensive step in reformulation checking for the output section is to ensure that the core constraints \(\mathcal {C}\) are included in the output formula and vice versa (possibly with permutations and duplicity). Here, CakePB normalizes all pseudo-Boolean constraints involved to a canonical form and then copies both \(\mathcal {C}\) and the output formula into respective array-backed hash tables for fast membership tests.

Optimizing Redundance and Checked Deletion Rules. A naïve implementation of these two rules would require iterating over the entire constraints database when checking all subproofs in (1) for the right-hand-side constraints \({{(\mathcal {C}\cup \mathcal {D}\cup \{ C \})}\!\!\upharpoonright _{\omega }} \cup \{ O\ge {{O}\!\!\upharpoonright _{\omega }} \}\). An important observation here is that preprocessing proofs frequently use substitutions \(\omega \) that only involve a small number of variables (often a single variable, which in addition is fresh in the important special case of reification constraints \( z \Leftrightarrow C \) encoding that z is true precisely when the constraint C is satisfied). Consequently, most of the constraints \({{(\mathcal {C}\cup \mathcal {D}\cup \{ C \})}\!\!\upharpoonright _{\omega }}\) can be skipped when checking redundance because they are unchanged by the substitution. Similarly, the constraint \(O\ge {{O}\!\!\upharpoonright _{\omega }}\) is expensive to construct when the objective \(O\) contains many terms, but this construction can be skipped if no variables being substituted occur in \(O\). CakePB stores a lazily-updated mapping of variables to their occurrences in the constraint database and the objective, which it uses to detect these cases.

The occurrence mapping just discussed is crucial for performance due to the frequency of steps involving witnesses for preprocessing proofs, but incurs some memory overhead in the checker. More precisely, every variable occurrence in any constraint in the database corresponds to exactly one ID in the mapping. Thus, the overhead of storing the mapping is in the worst case quadratic in the number of constraints, but it is still linear in the total space usage for the constraints database.

4.3 Verified WCNF Frontend

The CakePBwcnf frontend mediates between MaxSAT WCNF problems and pseudo-Boolean optimization problems native to CakePB. Accordingly, the correctness of CakePBwcnf is stated in terms of MaxSAT semantics, i.e., the encoding, underlying pseudo-Boolean semantics, and proof system are all formally verified. In order to trust CakePBwcnf, one only has to carefully inspect the formal definition of MaxSAT semantics shown in Fig. 3 to make sure that it matches the informal definition in Sect. 2.2. Here, each clause C is paired with a natural number n, where \(\textit{n} = 0\) indicates a hard clause and when \(\textit{n} > 0\) it is the weight of C. The optimal cost of a weighted CNF formula wfml is None (representing \(\infty \)) if no satisfying assignment to the hard clauses exist; otherwise, it is the minimum cost among all satisfying assignments to the hard clauses.

Fig. 3.
figure 3

Formalized semantics for MaxSAT WCNF problems.

Full size image

There and Back Again. CakePBwcnf contains a verified WCNF-to-PB encoder implementing the encoding described in Sect. 2.2. Its correctness theorems are shown in Fig. 4, where the two lemmas in the top row relate the satisfiability and cost of the WCNF to its PB optimization counterpart after running wcnf_to_pbf (and vice versa), see Observation 1. Using these lemmas, the final theorem (bottom row) shows that equioptimality for two (encoded) PB optimization problems can be translated back to equioptimality for the input and preprocessed WCNFs.

Fig. 4.
figure 4

Correctness theorems for the WCNF-to-PB encoding.

Full size image

Putting Everything Together. The final verification step is to specialize the end-to-end machine code correctness theorem for CakePB to the new frontend. The resulting theorem for CakePBwcnf is shown abridged in Fig. 5; a detailed explanation of similar CakeML-based theorems is available elsewhere [29, 69] so we do not go into details here. Briefly, the theorem says that whenever the verdict string “s VERIFIED OUTPUT EQUIOPTIMAL” is printed (as a suffix) to the standard output by an execution of CakePBwcnf, then the two input files given on the command line parsed to equioptimal MaxSAT WCNF instances.

Fig. 5.
figure 5

Abridged final correctness theorem for CakePBwcnf.

Full size image

5 Experiments

We updated the MaxSAT preprocessor MaxPre  2.1 [39, 42, 44] to MaxPre  2.2 which now produces proof logs in the VeriPB format [10]. MaxPre  2.2 is available at the MaxPre  2 repository [50]. The generated proofs were elaborated using VeriPB  [73] and then checked by the verified proof checker CakePBwcnf. As benchmarks we used the 558 weighted and 572 unweighted MaxSAT instances from the MaxSAT Evaluation 2023 [52].

The experiments were conducted on 11th Gen Intel(R) Core(TM) i5-1145G7 @ 2.60 GHz CPUs with 16 GB of memory, a solid state drive as storage, and Rocky Linux 8.5 as operating system. Each benchmark ran exclusively on a node and the memory was limited to 14 GB. The time for MaxPre was limited to 300 s. There is an option to let MaxPre know about this time limit, but we did not use this option since MaxPre then decides which techniques to try based on how much time remains. This would have made it very hard to get reliable measurements of the overhead when proof logging is switched on in the preprocessor. The time limits for both VeriPB and CakePBwcnf were set to 6000 s to get as many instances checked as possible.

The main focus of our evaluation was the default setting of MaxPre, which does not use some of the techniques mentioned in Sect. 3 (or the online appendix [40]). We also conducted experiments with all techniques enabled to check the correctness of the proof logging implementation for all preprocessing techniques. The data and source code from our experiments can be found in [41].

The goal of the experiments was to answer the following questions:

RQ1.:

How much extra time is required to write the proof for the preprocessor?

RQ2.:

How long does proof checking take compared to proof generation?

Fig. 6.
figure 6

Proof logging overhead for MaxPre.

Full size image
Fig. 7.
figure 7

MaxPre vs. combined proof checking running time.

Full size image

To answer the first question, in Fig. 6 we compare MaxPre with and without proof logging. In total, 1081 instances were successfully preprocessed by MaxPre without proof logging. With proof logging enabled, 8 fewer instances were preprocessed due to either time- or memory-outs. For the successfully preprocessed instances, the geometric mean of the proof logging overhead is 46% of the running time, and 95% of the instances were preprocessed with proof logging in at most twice the time required without proof logging.

Our comparison between proof generation and proof checking is based on the 1073 instances for which preprocessing with proof logging was successful. Out of these, 1021 instances were successfully checked and elaborated by VeriPB. For 991 instances the verdicts were confirmed by the formally verified proof checker CakePBwcnf, with the remaining instances being time- or memory-outs. This shows the practical viability of our approach, as the vast majority of preprocessing proofs were checked within the resource limits.

A scatter plot comparing the running time of MaxPre with proof logging enabled against the combined checking process is shown in Fig. 7. For the combined checking time, we only consider the instances that have been successfully checked by CakePBwcnf. In the geometric mean, the time for the combined verified checking pipeline of VeriPB elaboration followed by CakePBwcnf checking is \(113{\times }\) the preprocessing time of MaxPre. A general reason for this overhead is that the preprocessor has more MaxSAT application-specific context than the pseudo-Boolean checker, so the preprocessor can log proof steps without performing the actual reasoning while the checker must ensure that those steps are sound in an application-agnostic way. An example for this is reification: as the preprocessor knows its reification variables are fresh, it can easily emit redundance steps that witness on those variables; but the checker has to verify freshness against its own database. Similar behaviour has been observed in other applications of pseudo-Boolean proof logging [27, 37].

To analyse further the causes of proof checking overhead, we also compared VeriPB to CakePBwcnf. The checking of the elaborated kernel proof with CakePBwcnf is \(6.7{\times }\) faster than checking and elaborating the augmented proof with VeriPB. This suggests that the bottleneck for proof checking is VeriPB; VeriPB without elaboration is about \(5.3{\times }\) slower than CakePBwcnf. As elaboration is a necessary step before running CakePBwcnf, improving the performance of VeriPB would benefit the performance of the pipeline as a whole. One specific feature that seems desirable would be to augment RUP rule applications with LRAT-style hints [16], so that VeriPB would not need to perform unit propagation to elaborate RUP steps to cutting planes derivations. Though these types of engineering challenges are important to address, they are beyond the scope of the current paper and we have to leave them as future work.

6 Conclusion

In this work, we show how to use pseudo-Boolean proof logging to certify correctness of the MaxSAT preprocessing phase, extending previous work for the main solving phase in unweighted model-improving solvers [72] and general core-guided solvers [4]. As a further strengthening of previous work, we present a fully formally verified toolchain which provides end-to-end verification of correctness.

In contrast to SAT solving, there is a rich variety of techniques in maximum satisfiability solving, and it still remains to design pseudo-Boolean proof logging methods for general, weighted, model-improving MaxSAT solvers [21, 47, 62] and implicit hitting set (IHS) MaxSAT solvers [18, 19] with abstract cores [3]. Nevertheless, our work adds further weight to the conclusion that pseudo-Boolean reasoning seems like a very promising foundation for MaxSAT proof logging. We are optimistic that this work is another step on the path towards general adoption of proof logging in the context of SAT-based optimization.