Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Practically feasible proof logging for pseudo-Boolean optimization

Koops, Wietze LU orcid ; Le Berre, Daniel ; Myreen, Magnus O. ; Nordström, Jakob LU ; Oertel, Andy LU orcid ; Tan, Yong Kiam and Vinyals, Marc (2025) In Leibniz International Proceedings in Informatics (LIPIcs) 340. p.1-27
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... (More)
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. (Less)
Please use this url to cite or link to this publication:
author
; ; ; ; ; and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
Proc. of the 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)
series title
Leibniz International Proceedings in Informatics (LIPIcs)
volume
340
pages
27 pages
external identifiers
  • scopus:105013084285
ISBN
978-3-95977-380-5
DOI
10.4230/LIPIcs.CP.2025.21
project
Certified Linear Pseudo-Boolean Optimization
language
English
LU publication?
yes
id
b5de3846-96d8-4689-874a-e0e3f939175c
date added to LUP
2025-10-31 19:43:24
date last changed
2025-11-26 03:44:21
@inproceedings{b5de3846-96d8-4689-874a-e0e3f939175c,
  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.<br/><br/>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.}},
  author       = {{Koops, Wietze and Le Berre, Daniel and Myreen, Magnus O. and Nordström, Jakob and Oertel, Andy and Tan, Yong Kiam and Vinyals, Marc}},
  booktitle    = {{Proc. of the 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)}},
  isbn         = {{978-3-95977-380-5}},
  language     = {{eng}},
  month        = {{08}},
  pages        = {{1--27}},
  series       = {{Leibniz International Proceedings in Informatics (LIPIcs)}},
  title        = {{Practically feasible proof logging for pseudo-Boolean optimization}},
  url          = {{http://dx.doi.org/10.4230/LIPIcs.CP.2025.21}},
  doi          = {{10.4230/LIPIcs.CP.2025.21}},
  volume       = {{340}},
  year         = {{2025}},
}