ACL2 Seminar, April 30, 2013

Marijn Heule (speaker), Warren Hunt, and Nathan Wetzler

Efficient and Verified Checking of Unsatisfiability Proofs

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 wide-spread 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.