# Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability

arXiv: https://arxiv.org/abs/2501.17493 · HTML: https://mlsanity.com/paper/2501.17493/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 49 references that are in the map.
- First posted on arXiv 29 Jan 2025.

## Builds on (most cited first, 11 of 11)

- [MLIC: A MaxSAT-Based framework for learning interpretable classification rules](https://mlsanity.com/paper/1812.01843/) (2018)
- [Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs](https://mlsanity.com/paper/2209.12185/) (2022)
- [Efficient Certified RAT Verification](https://mlsanity.com/paper/1612.02353/) (2016)
- [Certified Symmetry and Dominance Breaking for Combinatorial Optimisation](https://mlsanity.com/paper/2203.12275/) (2022)
- [Incremental Cardinality Constraints for MaxSAT](https://mlsanity.com/paper/1408.4628/) (2014)
- [Generalized Totalizer Encoding for Pseudo-Boolean Constraints](https://mlsanity.com/paper/1507.05920/) (2015)
- [Efficient Certified Resolution Proof Checking](https://mlsanity.com/paper/1610.06984/) (2016)
- [Certified MaxSAT Preprocessing](https://mlsanity.com/paper/2404.17316/) (2024)
- [Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs](https://mlsanity.com/paper/2401.09277/) (2024)
- [New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization](https://mlsanity.com/paper/2204.10856/) (2022)
- [Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes](https://mlsanity.com/paper/2406.08175/) (2024)

## Built on by (most cited first, 2 of 2)

- [Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach](https://mlsanity.com/paper/2508.07015/) (2025)
- [Towards a Certifying Grounder](https://mlsanity.com/paper/2607.21199/) (2026)

## Abstract (arXiv)

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.