Trimming Pseudo-Boolean Proofs

Berhan Oumer Adame, Bart Bogaerts, Benjamin Bogø, Simon Dold, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, and Mark Turnbull
Submitted

Abstract

Modern combinatorial solvers are very efficient but also highly complex and therefore error-prone. The most successful approach to ensure correctness, proof logging, is now the accepted standard for Boolean satisfiability (SAT) solving, where proof trimming is an additional vital technique to reduce proof size and allow faster proof checking. However, efficient proof logging has remained a challenge for richer combinatorial paradigms, and trimming has not been supported for the more complex proof logging systems used. In this work, we present a proof trimmer covering the full VeriPB proof format, bringing the advantages of trimming to a wide range of paradigms such as MaxSAT, pseudo-Boolean optimisation, subgraph solving, and constraint programming. Our experimental evaluation demonstrates overall 6.37x proof size reductions and 1.81x total checking speedups (including formally verified proof checking).