Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs
Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs
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 …