Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability
Christoph Jabs, Jeremias Berg, Bart Bogaerts, Matti Järvisalo
TL;DR
Problem: certify Pareto-optimality in MO-MaxSAT when multi-objective proofs are not natively supported by VeriPB. Approach: embed Pareto-dominance into a fixed VeriPB preorder $\\mathcal{O}_P^\\mathbf{O}$ over objective variables, logging representative solutions for every non-dominated element without changing VeriPB, and instantiate proofs inside the MO-MaxSAT solver Scuttle with totalizer-encoded PB constraints. Contributions: (i) first end-to-end VeriPB-based proof logging for MO-MaxSAT, (ii) demonstration that PD cuts can be derived via redundance-based strengthening and solution logging, (iii) integration with P-minimal, LowerBound, and BiOptSat algorithms including core boosting, (iv) empirical overheads of $14\%-29\%$ on average and practical proof-checking costs. Significance: enables scalable, machine-verifiable certificates for MO-MaxSAT results, increasing trust in automated reasoning for multi-objective optimization.
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.