Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs

TL;DR

This paper introduces a novel method using pseudo-Boolean inequalities with extension variables to efficiently certify parity reasoning, significantly improving proof logging and verification times in combinatorial optimization problems.

Contribution

It presents a new proof logging approach that generalizes DRAT, enabling efficient certification of XOR reasoning and related paradigms in combinatorial optimization.

Findings

Dramatic reduction in proof logging and verification time.

Method generalizes DRAT format for broader problem types.

Enables certification of XOR reasoning in SAT solvers.

Abstract

The dramatic improvements in combinatorial optimization algorithms over the last decades have had a major impact in artificial intelligence, operations research, and beyond, but the output of current state-of-the-art solvers is often hard to verify and is sometimes wrong. For Boolean satisfiability (SAT) solvers proof logging has been introduced as a way to certify correctness, but the methods used seem hard to generalize to stronger paradigms. What is more, even for enhanced SAT techniques such as parity (XOR) reasoning, cardinality detection, and symmetry handling, it has remained beyond reach to design practically efficient proofs in the standard DRAT format. In this work, we show how to instead use pseudo-Boolean inequalities with extension variables to concisely justify XOR reasoning. Our experimental evaluation of a SAT solver integration shows a dramatic decrease in proof logging and verification time compared to existing DRAT methods. Since our method is a strict generalization of DRAT, and readily lends itself to expressing also 0-1 programming and even constraint programming problems, we hope this work points the way towards a unified approach for efficient machine-verifiable proofs for a rich class of combinatorial optimization paradigms.