Trimming Pseudo-Boolean Proofs

Abstract

Modern combinatorial solvers are very efficient but also highly complex and therefore error-prone. The most success- ful approach to ensure correctness—proof logging—is now the accepted standard for Boolean satisfiability (SAT) solving, where proof trimming is an additional crucial technique to reduce proof size and proof checking time. 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,