# Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs

arXiv: https://arxiv.org/abs/2209.12185 · HTML: https://mlsanity.com/paper/2209.12185/

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Sep 2022.

## Built on by (most cited first, 14 of 14)

- [Logic-Based Explainability in Machine Learning](https://mlsanity.com/paper/2211.00541/) (2022)
- [Certified MaxSAT Preprocessing](https://mlsanity.com/paper/2404.17316/) (2024)
- [Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability](https://mlsanity.com/paper/2501.17493/) (2025)
- [Formally Certified Approximate Model Counting](https://mlsanity.com/paper/2406.11414/) (2024)
- [Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach](https://mlsanity.com/paper/2508.07015/) (2025)
- [PBLean: Pseudo-Boolean Proof Certificates for Lean 4](https://mlsanity.com/paper/2602.08692/) (2026)
- [The Cardinality of Identifying Code Sets for Soccer Ball Graph with Application to Remote Sensing](https://mlsanity.com/paper/2407.14120/) (2024)
- [IGMaxHS -- An Incremental MaxSAT Solver with Support for XOR Clauses](https://mlsanity.com/paper/2410.15897/) (2024)
- [An Expansion-Based Approach for Quantified Integer Programming](https://mlsanity.com/paper/2506.04452/) (2025)
- [Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables](https://mlsanity.com/paper/2511.16637/) (2025)
- [Orbitopal Fixing in SAT](https://mlsanity.com/paper/2601.16855/) (2026)
- [LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean](https://mlsanity.com/paper/2607.28459/) (2026)
- [The Refutation Gap: Certifying Both Halves of an Optimality Claim](https://mlsanity.com/paper/2609.20873/) (2026)
- [RCShift: Certifying When Partial Linkage Suffices for Finite-Sample Decisions](https://mlsanity.com/paper/2609.26207/) (2026)

## Abstract (arXiv)

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.