ACL2 Seminar, June 19, 2013
Nathan Wetzler (joint work with Marijn Heule and Warren Hunt)

Title: Mechanical Verification of SAT Refutations with Extended Resolution

Abstract:

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.