Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals. Practically Feasible Proof Logging for Pseudo-Boolean Optimization. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 21:1-21:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CP.2025.21
Abstract:
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.
License type:
Attribution 4.0 International (CC BY 4.0)
Funding Info:
This research / project is supported by the Knut and Alice Wallenberg Foundation - Wallenberg AI, Autonomous Systems and Software Program (WASP)
Grant Reference no. : NA
This research / project is supported by the BLaSST ANR-21-CE25-0010 - NA
Grant Reference no. : NA
This research / project is supported by the Swedish Research Council - grant 2021-05165
Grant Reference no. : grant 2021-05165
This research / project is supported by the Swedish Research Council - grant 2016-00782
Grant Reference no. : grant 2016-00782
This research / project is supported by the Swedish Research Council - grant 2024-05801
Grant Reference no. : grant 2024-05801
This research / project is supported by the National Research Foundation - Singapore NRF Fellowship Programme
Grant Reference no. : NRF-NRFF16-2024-0002
This research / project is supported by the UoA FoS RDF 3729031 - NA
Grant Reference no. : NA