Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs

Authors

  • Stephan Gocht Lund University, Lund, Sweden University of Copenhagen, Copenhagen, Denmark
  • Jakob Nordström University of Copenhagen, Copenhagen, Denmark Lund University, Lund, Sweden

Keywords:

Satisfiability, Automated Reasoning and Theorem Proving, Satisfiability Modulo Theories

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.

Downloads

Published

2021-05-18

How to Cite

Gocht, S., & Nordström, J. (2021). Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5), 3768-3777. Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/16494

Issue

Section

AAAI Technical Track on Constraint Satisfaction and Optimization