Title: An Introduction to Pseudo-Boolean Proof Logging

Abstract: The output of current state-of-the-art combinatorial 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 a 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 talk I will instead discuss a proof logging scheme based on pseudo-Boolean constraints, i.e., 0-1 linear inequalities, with extension variables that has been shown to be applicable to various domains including constraint programming and subgraph-isomorphism solving as well as proof logging for parity reasoning within SAT solvers.