# Certified MaxSAT Preprocessing

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 81 references that are in the map.
- First posted on arXiv 26 Apr 2024.

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

- [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)
- [Efficient Certified Resolution Proof Checking](https://mlsanity.com/paper/1610.06984/) (2016)
- [Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs](https://mlsanity.com/paper/2401.09277/) (2024)

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

- [Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability](https://mlsanity.com/paper/2501.17493/) (2025)
- [PBLean: Pseudo-Boolean Proof Certificates for Lean 4](https://mlsanity.com/paper/2602.08692/) (2026)
- [Towards a Certifying Grounder](https://mlsanity.com/paper/2607.21199/) (2026)

## Abstract (arXiv)

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.