Abstract
Satisfiability (SAT) solvers—and software in general—sometimes have serious bugs. We mitigate these effects by validating the results. Today’s SAT solvers emit proofs that can be checked with reasonable efficiency. However, these checkers are not trivial and can have bugs as well. We propose to check proofs using a formally verified program that adds little overhead to the overall process of proof validation. We have implemented a sequence of increasingly efficient, verified checkers using the ACL2 theorem proving system, and we discuss lessons from this effort. This work is already being used in industry and is slated for use in the next SAT competition.
Cite
CITATION STYLE
Heule, M., Hunt, W., Kaufmann, M., & Wetzler, N. (2017). Efficient, verified checking of propositional proofs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10499 LNCS, pp. 269–284). Springer Verlag. https://doi.org/10.1007/978-3-319-66107-0_18
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
