Modern SAT solvers use preprocessing and inprocessing techniques that are not solely based on resolution; existing unsatisfiability proof formats do not support SAT solvers using such techniques. We present a new proof format for checking unsatisfiability proofs produced by SAT solvers that use techniques such as extended resolution and blocked clause addition. Our new format was designed with three goals: proofs should be easy to generate, proofs should be compact, and validating proofs must be simple. We show how existing preprocessors and solvers can be modified to generate proofs in our new format. Additionally, we implemented a mechanically-verified proof checker in ACL2 and a proof checker in C for the proposed format. © 2013 Springer-Verlag.
CITATION STYLE
Heule, M. J. H., Hunt, W. A., & Wetzler, N. (2013). Verifying refutations with extended resolution. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7898 LNAI, pp. 345–359). Springer Verlag. https://doi.org/10.1007/978-3-642-38574-2_24
Mendeley helps you to discover research relevant for your work.