Certified MaxSAT Preprocessing

TL;DR

This work extends certified proof logging to the preprocessing phase of MaxSAT, addressing a gap where prior certification focused mainly on core solving. By integrating pseudo-Boolean reasoning with end-to-end verification, the authors demonstrate that preprocessing steps can be proven equioptimal with respect to the original instance, using an extended VeriPB proof format and a verified CakePB checker. The approach results in a fully verified toolchain (including a new MaxSAT preprocessor, MaxPre) that logs reformulation steps and validates them against PB proofs, enabling reliable, certified preprocessing for real-world MaxSAT benchmarks. Experimental results indicate practical viability with manageable overhead, supporting broader adoption of certified MaxSAT preprocessing in applications requiring rigorous correctness guarantees.

Abstract

Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-hard optimization problems, but ensuring correctness of MaxSAT solvers has remained an important concern. For SAT, this is largely a solved problem thanks to the use of proof logging, meaning that solvers emit machine-verifiable proofs of (un)satisfiability to certify correctness. However, for MaxSAT, proof logging solvers have started being developed only very recently. Moreover, these nascent efforts have only targeted the core solving process, ignoring the preprocessing phase where input problem instances can be substantially reformulated before being passed on to the solver proper. In this work, we demonstrate how pseudo-Boolean proof logging can be used to certify the correctness of a wide range of modern MaxSAT preprocessing techniques. By combining and extending the VeriPB and CakePB tools, we provide formally verified, end-to-end proof checking that the input and preprocessed output MaxSAT problem instances have the same optimal value. An extensive evaluation on applied MaxSAT benchmarks shows that our approach is feasible in practice.

Figures (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.