Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability
This work addresses the need for verifiable correctness in automated reasoning systems, particularly for multi-objective optimization, but it is incremental as it adapts existing proof logging to a new context without extending the underlying format.
The paper tackles the problem of ensuring trustworthiness in multi-objective maximum satisfiability (MO-MaxSAT) solvers by enabling proof logging for the first time using the VeriPB format, showing empirically that this approach is scalable with reasonable overhead.
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.