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.

翻译：基于过去几十年来布尔可满足性（SAT）求解的进展，最大可满足性（MaxSAT）已成为解决NP难优化问题的可行方法，但确保MaxSAT求解器的正确性始终是一个重要关注点。对于SAT而言，由于使用了证明记录技术，这一问题已基本得到解决——求解器会输出机器可验证的可满足性/不可满足性证明以认证正确性。然而对于MaxSAT，证明记录求解器直到最近才开始被开发。此外，这些初步研究仅针对核心求解过程，忽略了预处理阶段——在该阶段，输入问题实例在传递给求解器前可能被大幅重构。本研究展示了如何利用伪布尔证明记录来认证现代MaxSAT预处理技术的正确性。通过结合并扩展VeriPB与CakePB工具，我们提供了形式化验证的端到端证明检查，确保输入与预处理后的MaxSAT问题实例具有相同的最优值。在实际MaxSAT基准测试上的广泛评估表明，该方法在实践中是可行的。