Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs - Gocht, Stephan; Nordström, Jakob (Proceedings of the AAAI Conference on Artificial Intelligence, 2021)
The dramatic improvements in combinatorial optimization algorithmsover the last decades have had a major impact in artificialintelligence, operations research, and beyond, but the output ofcurrent state-of-the-art solvers is often hard to verify and issometimes wrong. For Boolean satisfiability (SAT) solvers prooflogging has been introduced as a way to certify correctness, but themethods used seem hard to generalize to stronger paradigms. What ismore, even for enhanced SAT techniques such as parity (XOR) reasoning,cardinality detection, and symmetry handling, it has remained beyondreach to design practically efficient proofs in the standard DRATformat. In this work, we show how to instead use pseudo-Booleaninequalities with extension variables to concisely justify XORreasoning. Our experimental evaluation of a SAT solver integrationshows a dramatic decrease in proof logging and verification timecompared to existing DRAT methods. Since our method is a strictgeneralization of DRAT, and readily lends itself to expressing also0-1 programming and even constraint programming problems, we hope thiswork points the way towards a unified approach for efficientmachine-verifiable proofs for a rich class of combinatorialoptimization paradigms.