Reseña: Mechanical verification of SAT refutations with extended resolution

Se ha publicado un artículo de verificación formal en ACL2 titulado Mechanical verification of SAT refutations with extended resolution.

Sus autores son Nathan Wetzler, Marijn J. H. Heule y Warren A. Hunt Jr.

El trabajo se presentará en julio en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

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.