|
|
|---|
|
|
|
|---|
RAT Proof Checker for ITP 2013
This proof is the supplemental material for a paper appearing in Interactive Theorem Proving 2013. A README file describes the build process. Build, run, and clean scripts are provided for simplicity. The paper is available online as a preprint or from Springer.
We present a mechanically-verified proof checker developed with the ACL2 theorem-proving system that is general enough to support the growing variety of increasingly complex satisfiability (SAT) solver techniques, including those based on extended resolution. A common approach to assure the correctness of SAT solvers is to emit a proof of unsatisfiability when no solution is reported to exist. Contemporary proof checkers only check logical equivalence using resolution-style inference. However, some state-of-the-art, conflict-driven clause-learning SAT solvers use preprocessing, inprocessing, and learning techniques, that cannot be checked solely by resolution-style inference. We have developed a mechanically-verified proof checker that assures refutation clauses preserve satisfiability. We believe our approach is sufficiently expressive to validate all known SAT-solver techniques.
Mechanical verification of SAT refutations with extended resolution Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt, Jr. Interactive Theorem Proving (ITP), volume 7998 of LNCS, pages 229-244. Springer, 2013.