2026-07-21T03:11:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23882 2025-11-12T13:10:54Z ddc:004 open_access

Practically Feasible Proof Logging for Pseudo-Boolean Optimization Koops, Wietze Le Berre, Daniel Myreen, Magnus O. Nordström, Jakob Oertel, Andy Tan, Yong Kiam Vinyals, Marc proof logging certifying algorithms combinatorial optimization certification pseudo-Boolean solving 0-1 integer linear programming Certifying solvers have long been standard for decision problems in Boolean satisfiability (SAT), allowing for proof logging and checking with very limited overhead, but developing similar tools for combinatorial optimization has remained a challenge. A recent promising approach covering a wide range of solving paradigms is pseudo-Boolean proof logging, but this has mostly consisted of proof-of-concept works far from delivering the performance required for real-world deployment. In this work, we present an efficient toolchain based on VeriPB and CakePB for formally verified pseudo-Boolean optimization. We implement proof logging for the full range of techniques in the state-of-the-art solvers RoundingSat and Sat4j, including core-guided search and linear programming integration with Farkas certificates and cut generation. Our experimental evaluation shows that proof logging and checking performance in this much more expressive paradigm is now quite close to the level of SAT solving, and hence is clearly practically feasible. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Wietze Koops and Daniel Le Berre and Magnus O. Myreen and Jakob Nordström and Andy Oertel and Yong Kiam Tan and Marc Vinyals 2025 Is Part Of LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2025.21 urn:nbn:de:0030-drops-238825 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.21 eng https://creativecommons.org/licenses/by/4.0/legalcode