Efficient Certified Resolution Proof Checking
Lu\'is Cruz-Filipe, Joao Marques-Silva, Peter Schneider-Kamp

TL;DR
This paper introduces a new propositional proof tracing format that simplifies proof checking, enabling a highly efficient and certified proof checker, verified in Coq, to handle large SAT instances and a 200 TB proof of the Pythagorean Triples conjecture.
Contribution
The paper proposes a novel proof format and a certified proof checker, significantly improving efficiency and formal verification in propositional proof checking.
Findings
Checker outperforms state-of-the-art by two orders of magnitude
Certified checker performs comparably to non-certified tools on SAT instances
Successfully verified a 200 TB proof of the Pythagorean Triples conjecture
Abstract
We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms a state-of-the-art checker by two orders of magnitude. We then formalize the theory underlying propositional proof checking in Coq, and extract a correct-by-construction proof checker for our format from the formalization. An empirical evaluation using 280 unsatisfiable instances from the 2015 and 2016 SAT competitions shows that this certified checker usually performs comparably to a state-of-the-art non-certified proof checker. Using this format, we formally verify the recent 200 TB proof of the Boolean Pythagorean Triples conjecture.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
