Certifying Correctness for Combinatorial Algorithms: by Using Pseudo-Boolean Reasoning

Over the last decades, dramatic improvements in combinatorial
optimisation algorithms have significantly impacted artificial
intelligence, operations research, and other areas. These advances,
however, are achieved through highly sophisticated algorithms that are
difficult to verify and prone to implementation errors that can cause
incorrect results. A promising approach to detect wrong results is to
use certifying algorithms that produce not only the desired output but
also a certificate or proof of correctness of the output. An external
tool can then verify the proof to determine that the given answer is
valid. In the Boolean satisfiability (SAT) community, this concept is
well established in the form of proof logging, which has become the
standard solution for generating trustworthy outputs. The problem is
that there are still some SAT solving techniques for which proof
logging is challenging and not yet used in practice. Additionally,
there are many formalisms more expressive than SAT, such as constraint
programming, various graph problems and maximum satisfiability
(MaxSAT), for which efficient proof logging is out of reach for
state-of-the-art techniques.

This work develops a new proof system building on the cutting planes
proof system and operating on pseudo-Boolean constraints (0-1 linear
inequalities). We explain how such machine-verifiable proofs can be
created for various problems, including parity reasoning, symmetry and
dominance breaking, constraint programming, subgraph isomorphism and
maximum common subgraph problems, and pseudo-Boolean problems. We
implement and evaluate the resulting algorithms and a verifier for the
proof format, demonstrating that the approach is practical for a wide
range of problems. We are optimistic that the proposed proof system is
suitable for designing certifying variants of algorithms in
pseudo-Boolean optimisation, MaxSAT and beyond.