Abstract
Modern combinatorial optimization has had a major impact in science and industry. However, the problems considered are computationally very challenging, requiring increasingly sophisticated algorithm design, and there is a poor scientific understanding of how these complex algorithms, called combinatorial solvers, work. More importantly, even mature commercial solvers are known to sometimes produce wrong results, which can be fatal for some types of applications. One way to address this problem is to enhance combinatorial solvers with proof logging, meaning that they output not only solutions but also proofs of correctness. One can then feed the problem, solution, and proof to a dedicated proof checker to verify that there are no errors. Crucially, such proofs should require low overhead to generate and be easy to check, but should supply 100% guarantees of correctness. Our starting point in this presentation is the proof logging methods implemented with great success by the Boolean satisfiability (SAT) community. We will discuss some of the challenges that need to be overcome if proof logging is to be extended to more general paradigms in combinatorial optimization, or even to the full toolbox used in state-of-the-art SAT solvers. We will argue that moving from the clausal reasoning used in SAT proof logging to so-called pseudo-Boolean reasoning using 0-1 integer linear constraints seems to hit a sweet spot between making proofs simple and easy to verify while at the same time providing expressive power to support the sophisticated reasoning in MaxSAT solving, pseudo-Boolean optimization, and constraint programming.