Das Kapitel vertieft sich in die entscheidende Rolle automatisierten Denkens bei der Entwicklung korrekter und vertrauenswürdiger Systeme, wobei der Schwerpunkt auf Boolescher Zufriedenheit (SAT) und maximaler Zufriedenheit (MaxSAT) liegt. Es unterstreicht die Bedeutung von Nachweisprotokollierungs- und Überprüfungstechniken, um die Zuverlässigkeit der Lösergebnisse zu gewährleisten, insbesondere bei Optimierungsproblemen in der realen Welt. Der Text führt das VeriPB-Format ein, das Proof-Logging für Probleme bei der Optimierung von Einzelobjekten unterstützt und seine Anwendung auf Multiobjektiv-Lösungen von MaxSAT (MO-MaxSAT) ausweitet. Durch Nutzung von Vorbestellungen in VeriPB wird gezeigt, wie man Pareto-Optimalität in MO-MaxSAT-Algorithmen zertifiziert, um sicherzustellen, dass die berechneten Lösungen repräsentativ für den nicht dominierten Satz sind. Das Kapitel enthält detaillierte Proof-Logging-Prozeduren für verschiedene MO-MaxSAT-Algorithmen, darunter -minimal, BiOptSat und LowerBound, sowie die Kernvorverarbeitungstechnologie zur Steigerung der Leistungsfähigkeit. Experimentelle Ergebnisse zeigen, dass Proof Logging für MO-MaxSAT skalierbar gemacht werden kann, mit tolerierbaren Laufzeitkosten. Das Kapitel schließt mit der Diskussion der Implikationen dieser Erkenntnisse und potenzieller zukünftiger Arbeiten zur Ausweitung des Proof Logging auf alle Pareto-optimalen Lösungen.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Due to the wide employment of automated reasoning in the analysis and construction of correct systems, the results reported by automated reasoning engines must be trustworthy. For Boolean satisfiability (SAT) solvers—and more recently SAT-based maximum satisfiability (MaxSAT) solvers—trustworthiness is obtained by integrating proof logging into solvers, making solvers capable of emitting machine-verifiable proofs to certify correctness of the reasoning steps performed. In this work, we enable for the first time proof logging based on the VeriPB proof format for multi-objective MaxSAT (MO-MaxSAT) optimization techniques. Although VeriPB does not offer direct support for multi-objective problems, we detail how preorders in VeriPB can be used to provide certificates for MO-MaxSAT algorithms computing a representative solution for each element in the non-dominated set of the search space under Pareto optimality, without extending the VeriPB format or the proof checker. By implementing VeriPB proof logging into a state-of-the-art multi-objective MaxSAT solver, we show empirically that proof logging can be made scalable for MO-MaxSAT with reasonable overhead.
1 Introduction
Automated reasoning is central in enabling the analysis and construction of correct systems. Practical solvers developed in the realm of automated reasoning, such as Boolean satisfiability (SAT) solvers [9], facilitate the development of more complex automated reasoning systems. One successful example of such generic SAT-based approaches are solvers developed for maximum satisfiability (MaxSAT) [3]—the opti mization extension of SAT—enabling solving various NP-hard real-world optimization problems [3]. Further, SAT-based approaches are being generalized and developed for MaxSAT under multiple objectives, i.e., multi-objective MaxSAT [11, 13, 14, 29, 36‐38, 50, 51], with the aim of extending the success of MaxSAT to more efficiently solving real-world multi-objective optimization problems, from, e.g., staff scheduling [18] through package upgradeability [40] to finding interpretable classifiers [45].
The more SAT and MaxSAT solvers are used in real-world settings, the more important it is to be able to trust the results solvers provide. While solutions are generally easy to confirm, solvers should be trustworthy also when they report unsatisfiability or, in the context of optimization, when the solvers claim that a solution is optimal and hence no better solutions exist. In response to these concerns, proof logging and checking techniques for SAT solvers have been developed and widely adopted [15, 16, 28], among which DRAT [30, 31] remains today the de facto standard in the context of SAT solving. However, DRAT and other SAT proof formats work purely on propositional clauses, which makes them unsuitable for proof logging MaxSAT solvers. Instead, the VeriPB format [10, 27], which is based on pseudo-Boolean constraints (i.e., 0-1 linear inequalities) and offers direct support for reasoning about objective values in single-objective optimization problems, has enabled proof logging for various optimization contexts [7, 10, 17, 22‐27, 32, 33, 53], including MaxSAT solving [6, 7, 33, 52, 53].
Anzeige
In this work, we enable proof logging for various recently-proposed multi-objective MaxSAT solving techniques. To the best of our knowledge, this is the first work enabling proof logging in multi-objective optimization.1 Our solution builds on the VeriPB format. It is critical to note that VeriPB does not offer direct support for multiple objective functions, and is thereby seemingly restricted to proof logging single-objective optimization algorithms. However, as we will detail, proof logging for MO-MaxSAT can in fact be enabled without extending the VeriPB format or the proof checker. In particular, in order to provide certificates for MO-MaxSAT algorithms developed for computing a representative solution for each element in the so-called non-dominated set of the search space under Pareto optimality [21], we make in a specific way use of preorders supported by VeriPB. While preorders were first introduced to VeriPB for certifying symmetry and dominance breaking [10], here we show that, in fact, a single preorder suffices for certifying that an MO-MaxSAT algorithm has computed a representative solution at each element of the non-dominated set. As representative MO-MaxSAT techniques, we detail VeriPB-based proof logging for variants of the \(P\)-minimal [44, 50], BiOptSat [38], and LowerBound [14] approaches, as well as the recently-proposed MO-MaxSAT preprocessing/reformulation technique of core boosting [37] which has been shown to provide considerable runtime improvements to MO-MaxSAT solvers. By adding VeriPB proof logging to the implementations of these approaches in the MO-MaxSAT solver Scuttle [34, 36, 37], we show empirically that proof logging can be made scalable for MO-MaxSAT, with average proof logging overhead ranging from 14% to 29% depending on the solving approach.
2 Preliminaries
We begin with necessary preliminaries related to multi-objective MaxSAT and VeriPB proofs.
2.1 Clauses and Pseudo-boolean Constraints
A literal \(\ell \) is a \(\{0,1\}\)-valued Boolean variable \(x \) or its negation \(\overline{x} \equiv 1-x \). A propositional clause \(C = (\ell _1 \vee \ldots \vee \ell _k)\) is a disjunction of literals. A formula in conjunctive normal form (CNF) \(F = C _1 \wedge \ldots \wedge C _m\) is a conjunction of clauses. We often think of clauses as sets of literals and formulas as sets of clauses.
A (normalized) pseudo-Boolean (PB) constraint is a 0-1 linear inequality \(C = {\textstyle \sum }_{i} a _i \ell _i \ge b\) where \(a _i\) are positive integers and \(b\) a non-negative integer. We will assume wlog that all PB constraints are in normal form, meaning that the \(\ell _i\) are over different variables and all coefficients \(a _i\) and the bound are positive. A pseudo-Boolean (PB) formula is a conjunction (or set) of PB constraints. We identify the propositional clause \(C = (\ell _1 \vee \ldots \vee \ell _k)\) with the PB constraint \({\textstyle \sum }_{i=1}^k \ell _i \ge 1\). This is convenient as the algorithms and solvers that we develop proof logging for expect propositional clauses as input, and—as detailed in this work—produce their proofs in pseudo-Boolean format. If \(C \) is the PB constraint \(\sum _ia _i\ell _i\ge b\), we write \(\lnot C\) for its negation \(\sum _ia _i\overline{\ell _i} \ge \sum _ia _i - b + 1\). If p is a variable, we write \(p\Leftrightarrow C \) for the two constraints expressing that \(p\) implies \(C \) and vice versa, i.e., \(Mp + \sum _ia _i\overline{\ell _i} \ge M\) and \(b \overline{p} + \sum _ia _i\ell _i \ge b\) where \(M=\sum _ia _i -b +1\). An objective\(O\) is an expression \(\sum _i a _i \ell _i+L\) where the \(a _i\) and \(L\) are integers.
Anzeige
A substitution \(\omega \) maps each variable in its domain to a truth value (either 0 or 1) or to another literal. We denote by \(C \!\!\upharpoonright _{\!\omega }\) the constraint obtained from \(C \) by replacing each variable \(x \) in the domain of \(\omega \) by \(\omega (x)\); the notations \(O\!\!\upharpoonright _{\!\omega }\), \(F \!\!\upharpoonright _{\!\omega }\), and
for a tuple of variables
are defined analogously. An assignment \(\alpha \) is a substitution that maps only onto \(\{0,1\}\). When convenient, we view an assignment as the set of literals it sets to 1. An assignment \(\alpha \) is complete for a constraint, formula, or objective if \(\alpha \) maps each variable in them to a value, and partial otherwise. The assignment \(\alpha \) satisfies a constraint \(C \) if the constraint \(C \!\!\upharpoonright _{\!\alpha }= {\textstyle \sum }_{i} a '_i \ell '_i \ge b'\) obtained after normalization has \(b'=0\), and falsifies \(C \) if \({\textstyle \sum }_{i} a '_i < b'\). In other words, \(\alpha \) satisfies \(C \) if simplifying \(C \) by \(\alpha \) leads to a trivial constraint and falsifies \(C \) if no extension of \(\alpha \) satisfies \(C \). An assignment \(\alpha \) is a solution to a formula \(F \) if \(\alpha \) satisfies all constraints in \(F \). A constraint \(C \) is implied by \(F \) (denoted by \(F \models C \)) if all solutions of \(F \) also satisfy \(C \).
2.2 Multi-Objective MaxSAT
An instance \((F, \textbf{O})\) of multi-objective MaxSAT (MO-MaxSAT) consists of a CNF formula \(F \) and a set \(\textbf{O}= (O_1, \ldots , O_p)\) of p objectives under minimization. This definition for MO-MaxSAT captures standard (single-objective, weighted partial) MaxSAT by setting \(p=1\); see, e.g., [38]. Given two assignments \(\alpha \) and \(\beta \) that are complete for each \(O_i\), we say that \(\alpha \)weakly dominates\(\beta \) (and write \(\alpha \preceq _P\beta \)) if \(O_i\!\!\upharpoonright _{\!\alpha } \le O_i\!\!\upharpoonright _{\!\beta }\) holds for each \(i=1,\dots ,p\). Note that \(O\!\!\upharpoonright _{\!\alpha }\) is an integer value when \(\alpha \) is complete for \(O\). If additionally \(O_t\!\!\upharpoonright _{\!\alpha } < O_t\!\!\upharpoonright _{\!\beta }\) for some \(t\), we say that \(\alpha \)dominates\(\beta \) (and write \(\alpha \prec _P\beta \)). A solution \(\alpha \) to \(F \) is Pareto-optimal for \((F, \textbf{O})\) if \(\alpha \) is not dominated by any other solution to \(F \). The non-dominated set of \((F, \textbf{O})\) consists of the tuples of objective values of Pareto-optimal solutions, i.e., \(\{ (O_1\!\!\upharpoonright _{\!\alpha }, \ldots , O_p\!\!\upharpoonright _{\!\alpha }) \mid \alpha \text{ is } \text{ Pareto-optimal } \text{ for } (F, \textbf{O})\}\). Note that each element in the non-dominated set can correspond to several Pareto-optimal solutions. We focus on the task of computing a representative solution for each element of the non-dominated set.
Fig. 1.
A bi-objective MaxSAT instance and its Pareto-optimal solutions.
Example 1
Consider the bi-objective MaxSAT instance \((F,(O_1,O_2))\) in Fig. 1. Its non-dominated set is \(\{(4,8),(5,6),(6,3)\}\). Its three Pareto-optimal solutions are \(\{x _1,\overline{x _2},x _3,\overline{x _4},\overline{x _5} \}\), \(\{\overline{x _1},x _2,\overline{x _3},x _4,\overline{x _5} \}\), and \(\{\overline{x _1},\overline{x _2},x _3,x _4,\overline{x _5} \}\).
2.3 Multi-Objective MaxSAT Solving
We consider the multi-objective MaxSAT problem of finding a representative solution of each element in the non-dominated set. Various algorithms for this problem setting have been proposed recently [13, 14, 38, 50, 51]. These algorithms make incremental use of a SAT solver [19, 46] while adding constraints to the working formula, ending with an unsatisfiable working formula once all elements in the non-dominated set have been discovered.
For many of the existing algorithms for MO-MaxSAT, a crucial building block is what we call a Pareto-dominance cut, or PD cut for short. A PD cut is a (set of) constraint(s) that, given a solution \(\alpha \), is falsified exactly by all solutions that are weakly dominated by \(\alpha \) (including \(\alpha \) itself). Adding a PD cut to the working formula therefore excludes solutions weakly dominated by \(\alpha \) from further consideration. Note that for the single-objective case (\(p=1\)), a PD cut is identical to a solution-improving constraint, admitting only “better” solutions. This no longer holds when \(p>1\) since Pareto-dominance is not a total order: solutions that are incomparable to \(\alpha \) will satisfy the PD cut.
For objectives \(\textbf{O}=(O_1,\dots ,O_p)\) and solution \(\alpha \), let \(w_i\) be fresh variables for each \(O_i\) with their semantics defined by
The PD cut is the clause \((\overline{w_1} \vee \dots \vee \overline{w_p})\). For encoding (1), MO-MaxSAT algorithms use a choice of various CNF encodings [5, 20, 42, 43, 47]. We will return in more detail to how PD cuts are employed in the \(P\)-minimal [44, 50], LowerBound [14], and BiOptSat [38] algorithms in Section 3 when detailing VeriPB proof logging for each of these algorithms.
2.4 VeriPB
We now overview a simplified version of the VeriPB proof system, only discussing the rules that are relevant for our current exposition. For instance, while VeriPB supports single-objective optimization, we will only use the decision version of this proof system. We refer the interested reader to earlier work [10, 27] for an exposition of the full proof system.
Given a PB input formula \(F \), the VeriPB proof system maintains a proof configuration
, consisting of two sets of constraints, the core set\(\mathcal {C}\) and the derived set\(\mathcal {D}\), a pseudo-Boolean formula
over two tuples of variables
that do not appear in \(\mathcal {C}\), and a tuple of variables
. The core set can be thought of as being equal to \(F \) and the derived set as consisting of all constraints derived in the proof. The order \(\mathcal {O}\) defines a preorder \(\preceq \) on assignments as follows. If \(\alpha \) and \(\beta \) are assignments, then \(\alpha \preceq \beta \) iff
is true. The proof system will guarantee that \(\preceq \) is indeed a preorder, i.e., a reflexive and transitive relation. The preorder in this configuration was originally introduced in the context of symmetry and dominance breaking [10]. Here we will use the preorder for a different purpose and will in fact not use the dominance rule introduced in [10]. The precise role of the preorder in our proofs for MO-MaxSAT will be detailed in Section 3.
The configuration is initialized by setting \(\mathcal {C}=F \), \(\mathcal {D}=\emptyset \), \(\mathcal {O}=\emptyset \) (the empty, and hence trivially true formula) and
, the empty tuple. Afterwards, the configuration is updated using the rules detailed next.
New constraints can be added to \(\mathcal {D}\) by deriving them from previously derived constraints in \(\mathcal {C}\cup \mathcal {D}\) using the cutting planes proof system [12] consisting of the following rules.
Literal Axioms. For any literal \(\ell \), \(\ell \ge 0\) is an axiom and can be derived.
Linear Combination. Any positive integer linear combination of two previously derived PB constraints can be inferred.
Division. Given the normalized PB constraint \( \sum _i w_i \ell _i \ge A\) and a positive integer c, the constraint \( \sum _i \lceil w_i/c \rceil \ell _i \ge \lceil A/c \rceil \) can be inferred.
Conveniently, VeriPB also allows adding an implied constraint without giving an actual cutting planes derivation, namely, when the constraint is implied by reverse unit propagation (RUP), a generalization of the same notion in SAT [28]. RUP states that if applying integer bounds consistency propagation on \(\mathcal {C}\cup \mathcal {D}\cup \{\lnot C\}\) results in a contradiction, then C is implied by \(\mathcal {C}\cup \mathcal {D}\) and can hence be derived.
Additionally, VeriPB also allows for deriving non-implied constraints as long as the constraints are guaranteed to preserve satisfiability. Specifically VeriPB has the following generalization of the resolution asymmetric tautology (RAT) rule in SAT [41].
Redundance-Based Strengthening. The constraint C can be derived and added to \(\mathcal {D}\) given a substitution \(\omega \) and explicit (cutting planes) proofs for
i.e., explicit proofs that the constraint on the right is implied by the premises \(\mathcal {C}\cup \mathcal {D}\cup \{\lnot {C} \}\).
Intuitively, this rule ensures that \(\omega \) remaps any solution \(\alpha \) of \(\mathcal {C}\cup \mathcal {D}\) that does not satisfy C to a solution \(\alpha \circ \omega \) of \(\mathcal {C}\cup \mathcal {D}\) that (i) satisfies C and (ii) for which \(\alpha \circ \omega \preceq \alpha \), i.e., \(\alpha \circ \omega \) is least as good (in terms of the order) as \(\alpha \). A common application of redundance-based strengthening is reification: deriving two pseudo-Boolean constraints that encode \(\ell \Leftrightarrow D\) for some PB constraint \(D\in \mathcal {C}\cup \mathcal {D}\) and for some fresh literal \(\ell \).
In addition to adding constraints, previously derived constraints can also be deleted in order to reduce the number of constraints that the proof checker has to work with. However, deletion requires care. Without restrictions, deleting everything in \(\mathcal {C}\) could make an unsatisfiable formula satisfiable, which would clearly be incorrect. Deletion is allowed using the following rules.
Derived Deletion. Any constraint can be removed from \(\mathcal {D}\).
Core Deletion. A constraint C can be removed from \(\mathcal {C}\) if C can be derived from \(\mathcal {C}\setminus \{C\}\) with the redundance-based strengthening rule.
Solutions found are logged and excluded from further consideration by learning a constraint using the following rule.
Solution Logging. Given a solution \(\alpha \) to \(\mathcal {C}\cup \mathcal {D}\), we can derive the constraint \(\sum _{\ell \in \alpha }\overline{\ell } \ge 1\) that excludes \(\alpha \) and add this constraint to \(\mathcal {C}\).
Constraints can always be moved from the derived set to the core set using the transfer rule in order to allow, e.g., the application of core deletion.
Transfer Rule. If \(\mathcal {D}'\subseteq \mathcal {D}\), we can transfer from configuration
to
.
Finally, the order can be changed, provided that the derived set is empty (which can always be achieved using the transfer rule).
Order Change Rule. Given a proof in VeriPB format that \(\mathcal {O}'\) is reflexive (i.e.,
is trivial) and transitive (i.e., whenever
and
hold, so does
), and given a tuple of variables
of the right length, we can transition from
to
.
3 Proof Logging for Multi-Objective MaxSAT
As our main contributions, we will now detail how VeriPB can be used for enabling proof logging in the multi-objective setting—despite the fact that VeriPB does not directly support multiple objectives. Our solution is based on a new type of use of the preorder \(\mathcal {O}\) in VeriPB.
3.1 The General Setup
Preorders were originally introduced in VeriPB to enable proofs for symmetry breaking [10]. However, the preorder turns out to be applicable for multi-objective proof logging as well. Since all rules in VeriPB are guaranteed to preserve solutions that are minimal with respect to the defined preorder, the preorder generalizes a single objective \(O\): computing a solution optimal wrt \(O\) is equivalent to computing a solution that is smallest in the order \(\mathcal {O}^O\) defined by the formula that is true iff \(O\!\!\upharpoonright _{\!\alpha }\le O\!\!\upharpoonright _{\!\beta }\). As a first step towards the multi-objective setting, we introduce a suitable order for encoding Pareto-dominance. In the following definition, if
and
are two tuples of variables of equal length, we write
for the substitution that maps every \(u_i\) to \(v_i\) and all other variables to themselves.
Definition 1
Let \(\textbf{O}= (O_1,\dots ,O_p)\) be a tuple of \(p\) objectives over variables
, and define
over fresh variables
and
as the PB formula
.
The following proposition summarizes the properties of \(\mathcal {O}_P^\textbf{O}\) that are important for our setting.
Proposition 1
Let \(\textbf{O}= (O_1,\dots ,O_p)\) be a tuple of objectives and
the PB formula from Definition 1. Then the following hold:
\(\mathcal {O}_P^\textbf{O}\) encodes a preorder, i.e., a reflexive (
is trivially satisfied) and transitive (if
and
also
holds) relation.
is satisfied if and only if \(\alpha \preceq _P\beta \) wrt \(\textbf{O}\), i.e., if \(\alpha \) weakly dominates \(\beta \).
When the objectives are clear from context, we drop the superscript and use
for the order that encodes Pareto-dominance over the objectives.
With the transfer and order change rules, the order can be changed arbitrarily in VeriPB proofs. In our setting, however, we will use \(\mathcal {O}_P\) unchanged throughout the entire proof. From now on, a VeriPBproof for\((F,\textbf{O})\) refers to a standard VeriPB proof for \(F \) that (i) as the first derivation step loads the order \(\mathcal {O}_P\) over the variables
in the objectives \(\textbf{O}\), and (ii) at no other point in the proof changes the order. Our observations on valid VeriPB proofs assume that the conditions (i) and (ii) are satisfied. The VeriPB proof checker will not verify these two conditions for us; however, these are merely syntactic restrictions that can be verified easily (e.g., by checking that no other lines in the proof starts with load_order).
The following result now guarantees the correctness of the proofs produced for the different MO-MaxSAT algorithms.
Theorem 1
Let \(P\) be a VeriPB proof for \((F,\textbf{O})\) that derives a contradiction. Let S be the set of non-dominated solutions logged in \(P\), i.e., logged solutions that are not dominated by other solutions logged in \(P\). Then S contains a representative solution for each element in the non-dominated set of \((F,\textbf{O})\).
Let
be the proof configuration of \(P\) at step \(i\). From the additional conditions imposed for multi-objective proofs, we have \(\mathcal {O}_i = \mathcal {O}_P\) and
for all \(i \ge 1\), since \(\mathcal {O}_P\) over the variables
in \(\textbf{O}\) is loaded in the first derivation step.
Theorem 1 follows by the following lemmas. Lemma 1 is a restatement of the properties of VeriPB proofs shown in [10], included here for completeness.
Lemma 1
Let
be the \(i^{\text {th}}\) configuration of \(P\). For every solution \(\alpha \) of \(\mathcal {C}_i\), there exists a solution \(\beta \) of \(\mathcal {C}_i \cup \mathcal {D}_i\) for which
.
The next lemma establishes that no rule in \(\textsc {VeriPB} \) can “create” new non-dominated points.
Lemma 2
Consider the \(i^{\text {th}}\) configuration
of \(P\) for fixed \(i \ge 1\). Any solution of \(\mathcal {C}_i\) is weakly dominated by a Pareto-optimal solution of \((F,\textbf{O})\).
Proof
By induction on i. The base case \(i=1\) follows by Proposition 1 from the first configuration having \(\mathcal {C}_1 = F \). Assume that the statement holds for \(i-1\) and let
be the \(i{-}1^{\text {th}}\) configuration. The rules of \(\textsc {VeriPB} \) that can alter the core set are solution logging, core deletion, and the transfer rule. For the transfer rule, the statement follows immediately by Lemma 1. For solution logging, the result follows from any solution of \(\mathcal {C}_{i}\) being a solution of \(\mathcal {C}_{i-1}\). Assume thus that \(\mathcal {C}_i = \mathcal {C}_{i-1} \setminus \{C \}\) and let \(\alpha \) be a solution of \(\mathcal {C}_i\), that (for the non-trivial case) does not satisfy \(C \). We show that \(\alpha \) is weakly dominated by a Pareto-optimal solution of \((F, \textbf{O})\). By the properties of redundance-based strengthening and core deletion, there is a substitution \(\omega \) such that \(\beta = \alpha \circ \omega \) is a solution to \(\mathcal {C}_{i-1}\) for which
. By the induction assumption, \(\beta \) is weakly dominated by a Pareto-optimal solution \(\gamma \) of \((F, \textbf{O})\). Since \(\beta \preceq _P\alpha \), \(\alpha \) is weakly dominated by \(\gamma \). \(\square \)
Lemma 3 establishes that no rule except for solution logging can remove all representative solutions for an element in the non-dominated set of \((F, \textbf{O})\).
Lemma 3
Let
and
be the \(i{-}1^{\text {th}}\) and \(i^{\text {th}}\) configurations of \(P\), respectively. Assume that (i) the solutions of \(\mathcal {C}_{i-1} \cup \mathcal {D}_{i-1}\) include a representative for the non-dominated point \(\textbf{b}\) and (ii) the \(i^{\text {th}}\) configuration is obtained by a rule other than solution logging. Then the solutions of \(\mathcal {C}_{i} \cup \mathcal {D}_{i}\) include a representative solution for \(\textbf{b}\).
Proof
Let \(\alpha \) be the representative solution to \(\mathcal {C}_{i-1} \cup \mathcal {D}_{i-1}\) for \(\textbf{b}\). We construct a solution to \(\mathcal {C}_i \cup \mathcal {D}_i\) that is representative for \(\textbf{b}\). For the interesting case, assume that \(\alpha \) is not a solution to \(\mathcal {C}_i \cup \mathcal {D}_i\). By assumption the \(i^{\text {th}}\) configuration was reached by a rule other than solution logging, and hence \(\mathcal {D}_i = \mathcal {D}_{i-1} \cup \{C \}\) for a constraint \(C \) added using the redundance-based strengthening rule and a substitution \(\omega \). By redundance-based strengthening \(\beta = \alpha \circ \omega \) is a solution to \(\mathcal {C}_i \cup \mathcal {D}_i\) for which
. Hence by Proposition 1, \(\beta \) weakly dominates \(\alpha \). As \(\alpha \) is representative for the non-dominated point \(\textbf{b}\), \(\beta \) must be representative for \(\textbf{b}\) as well. \(\square \)
Using these three lemmas we can now establish Theorem 1 as follows.
Proof
(of Theorem1). Consider the first configuration
of \(P\), where \(\mathcal {C}_1 = F \) and \(\mathcal {D}_1 = \emptyset \). By Proposition 1, there is a one-to-one correspondence between the Pareto-optimal solutions of \((F,\textbf{O})\) and the solutions of \(\mathcal {C}_1 \cup \mathcal {D}_1\) that are minimal wrt \(\mathcal {O}_P\). Specifically, the solutions of \(\mathcal {C}_1 \cup \mathcal {D}_1\) contain a representative solution for each element in the non-dominated set of \((F,\textbf{O})\). Since \(P\) derives a contradiction, there are no solutions to the union of the core and derived set of the final configuration. Thus the theorem holds if (i) no solutions that dominate a Pareto-optimal solution of \((F, \textbf{O})\) are logged in the proof, and (ii) a representative solution for each element in the non-dominated set is logged in the proof. (i) follows by Lemma 2 and (ii) by Lemma 3. \(\square \)
We note that Theorem 1 also holds when an instance \((F, (O))\) only has a single objective. In this case \(\alpha \preceq _P\beta \) is equivalent to \(O\!\!\upharpoonright _{\!\alpha }\le O\!\!\upharpoonright _{\!\beta }\). Hence Theorem 1 states that the simplified version of VeriPB using only rules for decision problems (recall Section 2.4) is sufficient for certifying single-objective MaxSAT solvers as well. Thereby it can be argued that the (more complicated) optimization proof system presented in [10] could be simplified without losing any of its expressiveness by replacing the explicit linear objective and objective-specific rules by the linear order-based rules we describe.
3.2 Proof Logging for Pareto Dominance Cuts
A key step in proof logging the different multi-objective algorithms is the derivation of a constraint called a PD cut given a solution \(\alpha \). In particular, given a solution \(\alpha \) of \(F \), we will derive a constraint that states that we are no longer interested in solutions worse than or equally good as \(\alpha \) in terms of Pareto-dominance. In single-objective VeriPB, there is a dedicated rule that allows for deriving a so-called solution-improving constraint. However we will show that PD cuts can be derived only relying on the redundance-based strengthening and solution logging rules.
We will make use of some auxiliary variables \(w_i\) for each objective \(O_i\) (recall Equation (1)). Firstly, introducing such (reified) constraints can be done with redundance-based strengthening in a standard way [27]. The introduced constraints guarantee that iff \(\beta \) is worse than or equal to \(\alpha \) in \(O_i\), then variable \(w_i\) holds in \(\beta \). Now let \({\omega _\alpha }\) be the substitution that maps every variable to their value in \(\alpha \) and each \(w_i\) to 1. We claim that with the redundance-based strengthening rule and this witness we can derive the constraint
Intuitively, this constraint maps each solution weakly dominated by \(\alpha \) to \(\alpha \). In doing so it excludes all solutions the PD cut excludes (the solutions weakly dominated by \(\alpha \)) except for \(\alpha \) itself. To see that this constraint can be derived with redundance-based strengthening, we can verify that all proof obligations are indeed met.
For each constraint \(C \) in \(\mathcal {C}\cup \mathcal {D}\) that does not mention \(w_i\), \(C \!\!\upharpoonright _{\!\omega _\alpha }\) is trivially satisfied since \(\alpha \) is a solution that satisfies those constraints.
If \(C \) is one of the constraints (1), then clearly \(C \!\!\upharpoonright _{\!\omega _\alpha }\) holds too.
Clearly also \(C _\alpha \!\!\upharpoonright _{\!\omega _\alpha }\) holds.
Lastly, what we need to show is that
holds if \(C _\alpha \) is not satisfied. This constraint expresses that \(\alpha \) weakly dominates any assignment \(\beta \) that satisfies all derived constraints so far but not \(C _\alpha \). As such an assignment \(\beta \) must assign all \(w_i\) to 1, from (1) we immediately have that \(O_i\!\!\upharpoonright _{\!\beta }\ge O_i\!\!\upharpoonright _{\!\alpha }\), as desired.
Finally, after deriving \(C _\alpha \), we log the solution \(\alpha \) to obtain a solution-excluding constraint \(\sum _{\ell \in \alpha }\overline{\ell } \ge 1\). By adding \(\sum _{\ell \in \alpha }\overline{\ell } \ge 1\) to \(C _\alpha \), we arrive at \(\sum _{i=1}^p |\alpha |\cdot \overline{w_i} \ge 1\). Hence at least one of the \(w_i\) must be 0. Dividing the result by \(|\alpha |\) yields the PD cut \((\overline{w_1} \vee \dots \vee \overline{w_p})\).
Example 2
Recall the instance in Fig. 1. Table 1 shows the steps required in the VeriPB proof for certifying a PD cut based on solution \(\alpha = \{x _1,\overline{x _2},x _3,\overline{x _4},\overline{x _5} \}\) with objective values \((4,8)\). Steps \([a]\), \([b]\), \([c]\), and \([d]\) first introduce the definitions of the \(w^\alpha _1\) and \(w^\alpha _2\) variables from Equation (1) as normalized reified PB constraints. These steps are justified by redundance-based strengthening using the fresh variables \(w^\alpha _1\) and \(w^\alpha _2\) as witnesses. Next, step \([e]\) introduces \(C _\alpha \). Lastly, the solution \(\alpha \) is logged (in \([f]\)) and the PD cut derived (in \([g]\)).
Table 1.
Example proof for certifying a PD cut.
ID
Pseudo-Boolean Constraint
Comment
Justification
Input constraints and potential previous proof steps
To enforce bounds on the values of the different objectives, multi-objective MaxSAT algorithms make use of CNF encodings of (reified) pseudo-Boolean constraints. For certifying the correctness of MO-MaxSAT algorithms, the correctness of these encodings needs to be certified as well. All algorithms covered in this paper make use of the incremental (generalized) totalizer encoding [5, 42, 47]. The totalizer encoding can be visualized as a tree where each node has a set of output literals that “count” how many of the literals at the leaves of its subtree are \(1\). In earlier work [53] it has been shown how the clauses of the totalizer encoding can be derived in the VeriPB proof system from the constraints describing the semantics of the output and internal variables. For certifying the generalized totalizer encoding, the semantics of the output variables are slightly different. Each output variable \(o_b\) of a node is defined by the two constraints \( o_b \Leftrightarrow \sum _{i=1}^n a_i\ell _i \ge b \) over the \(n\) literals at the leaves of the subtree. In contrast to the unweighted case, \(a_i\) can be larger than 1 here and values of \(b\) that are not subsetsums of \(\{a_i \mid i=1,\dots ,n\}\) are omitted. Deriving the clauses of the generalized totalizer encoding now follows the cutting planes procedure described in [53].
Many implementations of MaxSAT algorithms employing the totalizer encoding only derive clauses for enforcing the \( o_b \Leftarrow \sum _{i=1}^n a_i\ell _i \ge b\) constraint, since these are enough for enforcing upper bounds on the objective values by setting \(o_b\) to \(0\). As observed in [38], for the generalized totalizer it is additionally necessary to enforce all output variables in the range \([b,\max \{a_i \mid i=1,\dots ,n\})\) to \(0\) in order to enforce \(\sum _{i=1}^n a_i\ell _i < b\). With this modification, also for the generalized totalizer encoding, deriving only one “direction” of clauses is enough from the perspective of the solver. In the proof, however, we will make use of both directions of the definition of these output variables; this means that a solution found by the SAT solver is not necessarily a solution to the constraints in the proof. When using a solution found by the SAT solver as a witness for the redundance-based strengthening rule for deriving a PD cut (recall Section 3.2), we therefore need to adjust the assignment to satisfy the stricter semantics of the proof first. This is done during proof generation by traversing through all nodes of the (generalized) totalizer encodings and manually assigning the output variables to values following the strict semantics described above. This adjusted assignment is still guaranteed to satisfy all clauses in the SAT solver.
Next, we detail three state-of-the-art MO-MaxSAT algorithms and how to generate proofs for them.
P-minimal [44, 50]. Starting from any solution \(\alpha \), the \(P\)-minimal algorithm introduces a PD cut excluding all solutions that are weakly dominated by \(\alpha \). A SAT solver is then queried while temporarily enforcing the next-found solution to dominate \(\alpha \). Both steps are achieved using the generalized totalizer encoding. If no solution dominating the latest one can be found, the previous solution is guaranteed to be Pareto-optimal. In this case \(P\)-minimal drops the temporary constraints and starts over. If the working formula is unsatisfiable at this point, \(P\)-minimal terminates. An example of a search path of \(P\)-minimal in objective space is illustrated on the left-hand side of Fig. 2. The blue circles and red dots represent the solutions found by the SAT solver, with the red dots representing Pareto-optimal solutions. In such an execution, \(P\)-minimal introduces a PD cut for each of these solutions.
Fig. 2.
Illustrations of the search path of MO-MaxSAT algorithms in objective space.
For proof logging \(P\)-minimal we certify the generalized totalizer objective encodings and the added PD cuts in the VeriPB proof (as already described). This allows a contradiction to be derived in the proof iff a PD cut was added for each element in the non-dominated set. The temporary constraints that enforce domination are not required in the proof since they are merely heuristics guiding the SAT solver to certain regions temporarily and are not needed for reaching the final contradiction.
LowerBound [14]. The LowerBound algorithm restricts the search space by temporarily enforcing upper bounds of the form \(O_i \le b_i\) on each objective and then executes \(P\)-minimal within these bounds. Once \(P\)-minimal terminates, the bounds \(b_i\) are loosened and the process is repeated. LowerBound terminates once the bounds include the entire search space. In this last case, \(P\)-minimal is executed without the temporary bound constraints and will terminate with an unsatisfiable working instance. For proof logging LowerBound it therefore suffices to proof log the invocations of \(P\)-minimal as a subroutine. The search path for one invocation of \(P\)-minimal within a set of bounds is illustrated in green in Fig. 2 (middle).
BiOptSat [38]. The BiOptSat algorithm is specific to problems with two objectives \((O_1, O_2)\). The algorithm enumerates non-dominated points under the guarantee that the values for one objective are monotonically increasing, while the values of the other objective are decreasing. BiOptSat first employs the subroutine MinInc to minimize \(O_1\) without any additional constraints, returning the solution \(\alpha \). Next, the subroutine MinDec uses solution-improving search to minimize \(O_2\) under the condition that \(O_1 = O_1\!\!\upharpoonright _{\!\alpha }\). Let the final solution found by MinDec be \(\beta \), which is guaranteed to be Pareto-optimal. BiOptSat then repeats this process after introducing the constraint \(O_2 \le O_2\!\!\upharpoonright _{\!\beta }- 1\). An example of a search path of BiOptSat is illustrated in Fig. 2 (right). Since MinInc finds the global minimum of \(O_1\) for the current working formula, assume for now that we have a proof logging procedure for MinInc that results in the constraint \(C _\texttt {MinInc}:= O_1 \ge O_1\!\!\upharpoonright _{\!\alpha }\) being added to the proof. For any solution found during the execution of MinDec, we introduce a PD cut, which in turn is strengthened to the unit clause \((\overline{w_2})\) by combining it with \(C _\texttt {MinInc} \). This strengthened PD cut is semantically equivalent to the constraint added during solution-improving search in MinDec and at the end before BiOptSat starts over.
Example 3
Recall again the instance in Fig. 1. Assume that we have executed MinInc and MinDec once already and that MinDec has yielded the Pareto-optimal \(\alpha = \{x _1,\overline{x _2},x _3,\overline{x _4},\overline{x _5} \}\). Table 2 details the proof steps taken to certify the constraint \(O_2 < O_2\!\!\upharpoonright _{\!\alpha }\) added as the last step in BiOptSat. First, assume that \([lb]\) is \(C _\texttt {MinInc} \) derived in the proof during MinInc. Next, we certify the PD cut for \(\alpha \) in the proof as detailed in Table 1. Finally, by summing up the lower-bounding constraint from MinInc, the definition of \(w^\alpha _1\) and the PD cut, we obtain \(\overline{w^\alpha _2} \ge 1\) which is semantically equivalent to the constraint added by BiOptSat.
Table 2.
Example proof for a strengthened PD cut in BiOptSat.
ID
Pseudo-Boolean Constraint
Comment
Justification
Input constraint and potential previous proof steps
It remains to show that we can proof log MinInc to derive \(C _\texttt {MinInc} \). The details depend on the implementation of MinInc for which several variants have been proposed [38]. For the SAT-UNSAT variant, where MinInc is implemented as solution-improving search, \(C _\texttt {MinInc} \) is implicitly derived by the SAT solver during the final unsatisfiable query. Proof logging for the core-guided variants of MinInc can be implemented as already described for the single-objective setting in [7]; in short, \(C _\texttt {MinInc} \) can be derived from the final reformulated objective.
3.4 Proof Logging Core Boosting
Core boosting [37] is a recently-proposed preprocessing/reformulation technique for MO-MaxSAT, consisting of applying the single-objective core-guided optimization algorithm OLL [2, 48] wrt each objective individually, before executing an MO-MaxSAT algorithm on the reformulated objectives obtained from OLL. With this, core boosting shrinks the search space that needs to be considered by the MO-MaxSAT algorithm by deriving lower bounds for each objective. Core boosting also alters the structure of the CNF objective encodings since the totalizer structures built by OLL during core boosting can be reused in the objective encodings built by the MO-MaxSAT algorithm.
We give a brief overview of the single-objective core-guided OLL MaxSAT algorithm to the extent relevant for understanding how proof logging for core boosting works. Given an objective \(O\), OLL invokes a SAT solver with the assumptions that none of the literals in \(O\) incurs cost. If these assumptions are not satisfiable, the SAT solver returns an implied clause \(C \)—referred to as an unsatisfiable core—over the objective literals. OLL now introduces counting variables \(o_i \Leftarrow \sum _{\ell \in C} \ell \ge i\) for \(i=2,\dots ,|C |\) (encoded by the totalizer encoding) and reformulates the objective by adding \(c_C \cdot (\sum _{\ell \in C} -\ell + \sum _{i=2}^{|C |} o_i + 1)\) to it, where \(c_C \) is the minimum objective coefficient of any literals in \(C \). Iteratively applying this process guarantees that the reformulated objective is always equal to the original objective and OLL terminates once there is a solution that does not incur cost on any of the literals in the reformulated objective.
Example 4
Let \(O= x _1 + x _2 + x _3 + 2 x _4\) be one of the objectives that core boosting is performed on. Assume the first core extracted is \(C _1 = (x _1 \vee x _2 \vee x _3 \vee x _4)\). OLL reformulates \(C _1\) by adding counting variables \(a_i \Leftarrow x _1 + x _2 + x _3 + x _4 \ge i\) for \(i=2,3,4\). Assume the next core extracted is \(C _2 = (x _4 \vee a_2)\), which is reformulated by adding the counting variable \(b_2 \Leftarrow x _4 + a_2 \ge 2\). The final reformulated objective is \(O' = a_3 + a_4 + b_2 + 2\).
Proof logging for OLL is described in [7], yielding a constraint of form \(O\ge O'\) associating the reformulated objective \(O'\) with the original objective \(O\). After OLL has been executed, core boosting builds a CNF encoding for each reformulated objective. However, if the reformulated objective contains a sequence of literals that are outputs for the same totalizer, they should be reused as an internal node of the final encoding employed by the MO-MaxSAT algorithm rather than individual leaves. This avoids introducing new auxiliary variables that would end up being equivalent to the variables introduced by OLL.
Example 5
Figure 3 (left and middle-left, respectively) shows the two totalizer encodings built by OLL, where \(\square \) denotes the output variable with value 1 that is omitted by OLL. Figure 3 (middle-right) shows the encoding of the reformulated objective built by core boosting after executing OLL, where \(a_3,a_4\) is reused as an internal node. The dashed box shows the encoding that would be built when treating \(a_3\) and \(a_4\) individually. Since \(a_3\) and \(a_4\) are already totalizer outputs, \(d_1\) and \(d_2\) in this structure are equivalent to \(a_3\) and \(a_4\) and therefore redundant.
Fig. 3.
An objective encoding structure built by core boosting. The dashed box shows the alternative structure that would be built without reusing \(a_3,a_4\) as an internal node.
Going beyond previous work, certifying the encoding of the reformulated objective built during core boosting requires special care. In particular, due to the process of reusing partial sequences of totalizer output variables as internal nodes, using the semantics of the totalizer outputs built by OLL does not allow us to derive the clauses required for the encoding. Instead, for a sequence of variables \(o_r,\dots ,o_{r+n}\) reused as an internal node in the encoding, we introduce ordering constraints
$$ C ^{a}_v := \sum _{i=r}^{v} [\overline{o_i} \ge 0] + \sum _{i=v+1}^{r+n} [\overline{o_i} + o_v \ge 1] = \left[ M o_v + \sum _{i=r}^{r+n} \overline{o_i} \ge M \right] , $$
for each \(v=r,\dots ,r+n\). These constraints sum up axioms and ordering constraints, which can be derived from the semantic definitions of the totalizer output variables, and are therefore derivable in the proof. Furthermore, \(C ^{a}_v,C ^{b}_v\) are identical to \(o_v \Leftrightarrow \sum _{i=r}^{r+n} o_i \ge (v-r)\). When deriving the clauses involving the reused output variable sequence, we therefore use \(C ^{a}_v\) and \(C ^{b}_v\) instead of the semantic definitions of the variables, which allows for deriving the clauses of the encoding.
After core boosting, the output variables of the objective encoding are now defined with respect to the reformulated objective rather than the original one. As a final step, after certifying a PD cut with respect to the original objectives, we therefore use the objective reformulation constraints derived while executing OLL to certify the PD cut with respect to the reformulated objectives.
Example 6
All required clauses for the encoding shown in Fig. 3 (middle-right) can be derived from the semantic definitions \(c_i \Leftrightarrow a_3 + a_4 + b_2 \ge i\) for \(i=1,2,3\) while treating the individual variable \(b_2\) as a leaf and using \(C ^{a}\) and \(C ^{b}\) as “pseudo semantics” for the node \(a_3,a_4\). Note that the semantics for \(c_i\) are with respect to the variable part of the reformulated objective.
4 Experiments
We extended all algorithms implemented in the Scuttle [34, 36, 37] MO-MaxSAT solver—namely, \(P\)-minimal [44, 50], LowerBound [14], and (the SAT-UNSAT variant of) BiOptSat [38], each with and without core boosting—with the just-described VeriPB proof logging. We used CaDiCaL 2.0.0 [8] as the SAT solver within Scuttle and the VeriPB 2.2.2 proof checker [1] for checking the produced proofs.2 The proof logging Scuttle implementation is available in open source [34, 39]. We evaluate the implementation on the same set of benchmark instances used in the original work proposing core boosting [37]. This set of benchmarks consists of 300 instances from 6 domains with the number of objectives ranging from 2 to 5. The experiments were run on 2.50-GHz Intel Xeon Gold 6248 machines with 381-GB RAM in RHEL under a 32-GB memory limit and 1 hour time limit for Scuttle.
Table 3.
Average proof logging overheads and average proof checking overheads.
The per-instance Scuttle runtimes for each benchmark domain with and without proof logging are shown in Fig. 4 for all three MO-MaxSAT algorithms in Scuttle, both with and without core boosting. We observe that the runtime overhead of proof logging is in all cases quite tolerable, with average runtime increase ranging from 14% to 29% depending on the algorithm; see Table 3 for details. There are at most 3 instances (for \(P\)-minimal without core boosting) that were only solved without proof logging within the given 1-h time limit. While this work is not focussed on improving proof checking but rather realizing for the first time proof logging in a multi-objective setting, Table 3 also includes the proof checking overhead, i.e., (proof checking time)/(Scuttle runtime with proof logging), resulting from checking the Scuttle proofs with the VeriPB checker. With a time limit of 10 hours enforced for the VeriPB checker, we observed that checking takes on average 1–1.5 orders of magnitude more time than solving the instances with proof logging enabled. It should be noted that similar observations have been made, e.g., in the realm of VeriPB-based certified MaxSAT preprocessing [33]. Indeed, these observations motivate seeking improvements to the current runtime performance of the VeriPB checker. We observed that in cases, in particular for \(P\)-minimal (see the appendix in the extended version on arXiv [35] for more details), the proof checking overhead appears to somewhat correlate with the number of PD cuts produced during search.
5 Conclusions
We realized for the first time proof logging for multi-objective MaxSAT solving. Circumventing the fact that VeriPB does not offer direct support for multiple objectives, we detailed how preorders in VeriPB can be used to provide certificates for MO-MaxSAT algorithms that compute a representative solution for each element of the non-dominated set (with respect to the Pareto order). We achieved this without changes to the VeriPB format or the proof checker. Integrating VeriPB proof logging into a state-of-the-art multi-objective MaxSAT solver, we empirically showed that proof logging can be made scalable for MO-MaxSAT. While we in this work detailed how VeriPB can be employed for proof logging SAT-based multi-objective approaches, the same concepts are applicable to enabling proof logging for similar algorithmic ideas instantiated for other contexts, e.g., in the context of pseudo-Boolean optimization. Developing proof logging methods that capture the computation of all Pareto-optimal solutions, i.e., every solution at each element in the non-dominated set, potentially by extending VeriPB, also remains part of future work.
Acknowledgments
We thank Armin Biere, Katalin Fazekas, and Florian Pollitt for their help in fixing some bugs in CaDiCaL, and Andy Oertel for fixing a bug in the VeriPB proof checker. This work is partially funded by Research Council of Finland (grants 356046 and 362987) and the European Union (ERC, CertiFOX, 101122653). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Although relatively distant to the present work, there is some work on certificates in the context of multi-objective queries in Markov decision processes [4].
for a tuple of variables
are defined analogously. An assignment \(\alpha \) is a substitution that maps only onto \(\{0,1\}\). When convenient, we view an assignment as the set of literals it sets to 1. An assignment \(\alpha \) is complete for a constraint, formula, or objective if \(\alpha \) maps each variable in them to a value, and partial otherwise. The assignment \(\alpha \) satisfies a constraint \(C \) if the constraint \(C \!\!\upharpoonright _{\!\alpha }= {\textstyle \sum }_{i} a '_i \ell '_i \ge b'\) obtained after normalization has \(b'=0\), and falsifies \(C \) if \({\textstyle \sum }_{i} a '_i < b'\). In other words, \(\alpha \) satisfies \(C \) if simplifying \(C \) by \(\alpha \) leads to a trivial constraint and falsifies \(C \) if no extension of \(\alpha \) satisfies \(C \). An assignment \(\alpha \) is a solution to a formula \(F \) if \(\alpha \) satisfies all constraints in \(F \). A constraint \(C \) is implied by \(F \) (denoted by \(F \models C \)) if all solutions of \(F \) also satisfy \(C \).
, consisting of two sets of constraints, the core set \(\mathcal {C}\) and the derived set \(\mathcal {D}\), a pseudo-Boolean formula
over two tuples of variables
that do not appear in \(\mathcal {C}\), and a tuple of variables
. The core set can be thought of as being equal to \(F \) and the derived set as consisting of all constraints derived in the proof. The order \(\mathcal {O}\) defines a preorder \(\preceq \) on assignments as follows. If \(\alpha \) and \(\beta \) are assignments, then \(\alpha \preceq \beta \) iff
is true. The proof system will guarantee that \(\preceq \) is indeed a preorder, i.e., a reflexive and transitive relation. The preorder in this configuration was originally introduced in the context of symmetry and dominance breaking [10]. Here we will use the preorder for a different purpose and will in fact not use the dominance rule introduced in [10]. The precise role of the preorder in our proofs for MO-MaxSAT will be detailed in Section 3.
, the empty tuple. Afterwards, the configuration is updated using the rules detailed next.
to
.
is trivial) and transitive (i.e., whenever
and
hold, so does
), and given a tuple of variables
of the right length, we can transition from
to
.
and
are two tuples of variables of equal length, we write
for the substitution that maps every \(u_i\) to \(v_i\) and all other variables to themselves.
, and define
over fresh variables
and
as the PB formula
.
the PB formula from Definition 1. Then the following hold:
is trivially satisfied) and transitive (if
and
also
holds) relation.
is satisfied if and only if \(\alpha \preceq _P\beta \) wrt \(\textbf{O}\), i.e., if \(\alpha \) weakly dominates \(\beta \).
for the order that encodes Pareto-dominance over the objectives.
in the objectives \(\textbf{O}\), and (ii) at no other point in the proof changes the order. Our observations on valid VeriPB proofs assume that the conditions (i) and (ii) are satisfied. The VeriPB proof checker will not verify these two conditions for us; however, these are merely syntactic restrictions that can be verified easily (e.g., by checking that no other lines in the proof starts with 
be the proof configuration of \(P\) at step \(i\). From the additional conditions imposed for multi-objective proofs, we have \(\mathcal {O}_i = \mathcal {O}_P\) and
for all \(i \ge 1\), since \(\mathcal {O}_P\) over the variables
in \(\textbf{O}\) is loaded in the first derivation step.
be the \(i^{\text {th}}\) configuration of \(P\). For every solution \(\alpha \) of \(\mathcal {C}_i\), there exists a solution \(\beta \) of \(\mathcal {C}_i \cup \mathcal {D}_i\) for which
.
of \(P\) for fixed \(i \ge 1\). Any solution of \(\mathcal {C}_i\) is weakly dominated by a Pareto-optimal solution of \((F,\textbf{O})\).
be the \(i{-}1^{\text {th}}\) configuration. The rules of \(\textsc {VeriPB} \) that can alter the core set are solution logging, core deletion, and the transfer rule. For the transfer rule, the statement follows immediately by Lemma 1. For solution logging, the result follows from any solution of \(\mathcal {C}_{i}\) being a solution of \(\mathcal {C}_{i-1}\). Assume thus that \(\mathcal {C}_i = \mathcal {C}_{i-1} \setminus \{C \}\) and let \(\alpha \) be a solution of \(\mathcal {C}_i\), that (for the non-trivial case) does not satisfy \(C \). We show that \(\alpha \) is weakly dominated by a Pareto-optimal solution of \((F, \textbf{O})\). By the properties of redundance-based strengthening and core deletion, there is a substitution \(\omega \) such that \(\beta = \alpha \circ \omega \) is a solution to \(\mathcal {C}_{i-1}\) for which
. By the induction assumption, \(\beta \) is weakly dominated by a Pareto-optimal solution \(\gamma \) of \((F, \textbf{O})\). Since \(\beta \preceq _P\alpha \), \(\alpha \) is weakly dominated by \(\gamma \). \(\square \)
and
be the \(i{-}1^{\text {th}}\) and \(i^{\text {th}}\) configurations of \(P\), respectively. Assume that (i) the solutions of \(\mathcal {C}_{i-1} \cup \mathcal {D}_{i-1}\) include a representative for the non-dominated point \(\textbf{b}\) and (ii) the \(i^{\text {th}}\) configuration is obtained by a rule other than solution logging. Then the solutions of \(\mathcal {C}_{i} \cup \mathcal {D}_{i}\) include a representative solution for \(\textbf{b}\).
. Hence by Proposition 1, \(\beta \) weakly dominates \(\alpha \). As \(\alpha \) is representative for the non-dominated point \(\textbf{b}\), \(\beta \) must be representative for \(\textbf{b}\) as well. \(\square \)
of \(P\), where \(\mathcal {C}_1 = F \) and \(\mathcal {D}_1 = \emptyset \). By Proposition 1, there is a one-to-one correspondence between the Pareto-optimal solutions of \((F,\textbf{O})\) and the solutions of \(\mathcal {C}_1 \cup \mathcal {D}_1\) that are minimal wrt \(\mathcal {O}_P\). Specifically, the solutions of \(\mathcal {C}_1 \cup \mathcal {D}_1\) contain a representative solution for each element in the non-dominated set of \((F,\textbf{O})\). Since \(P\) derives a contradiction, there are no solutions to the union of the core and derived set of the final configuration. Thus the theorem holds if (i) no solutions that dominate a Pareto-optimal solution of \((F, \textbf{O})\) are logged in the proof, and (ii) a representative solution for each element in the non-dominated set is logged in the proof. (i) follows by Lemma 2 and (ii) by Lemma 3. \(\square \)
holds if \(C _\alpha \) is not satisfied. This constraint expresses that \(\alpha \) weakly dominates any assignment \(\beta \) that satisfies all derived constraints so far but not \(C _\alpha \). As such an assignment \(\beta \) must assign all \(w_i\) to 1, from (1) we immediately have that \(O_i\!\!\upharpoonright _{\!\beta }\ge O_i\!\!\upharpoonright _{\!\alpha }\), as desired.
