Efficient and Verified Checking of Unsatisfiability Proofs

Presented as part of the 2013 HCSS conference.

ABSTRACT

Satisfiability (SAT) solvers act as the core search engine in many tools used for bounded model checking and the verification of hardware and software.  It is incumbent upon these solvers to produce correct results.  For many tools, such as theorem provers, trusting the results of SAT solvers is not enough; they should be verified. Two problems obstruct widespread verification of unsatisfiability results: checking proofs can be very expensive and existing checking procedures cannot verify all existing techniques used in modern SAT solvers.  We tackle both problems by introducing a new clausal proof format that allows efficient checking of all existing SAT solving techniques. Our proposed method has one disadvantage: a fast checker for the new format is more complex as compared to checkers for existing formats.  We deal with this issue by creating a proof compressor that reduces the size of unsatisfiability proofs significantly.  The compact proof can be validated using a simple verified checker.  We implemented and mechanically verified such a proof checker using the ACL2 theorem prover.