Duration: 1:37:53

180 views

3

We present recent work on validating satisfiability refutations. Satis?ability (SAT) is considered as one of the most important core technologies in formal verification and related areas. SAT solvers are used not only to find a solution for a Boolean formula, but also to make the claim that no solution exists. In most applications of SAT, the absence of a solution represents the absence of errors in a design. When no solution is reported to exist, a solver can emit a proof of unsatisfiability, or refutation, which can then be validated by a proof checker. We have designed a new proof format that uses a solver's deletion information to significantly reduce checking time. Emitting a refutation in our format requires minor modifications to contemporary SAT solvers and preprocessors. We have also developed a proof checking tool for the new format which validates refutations in a time similar to the solving time. Our tool was used to check the unsatisfiability results of the SAT Competition 2013. We believe that it is now practical for SAT solvers to include this proof-checking capability; this will increase our confidence in SMT solvers and theorem provers that use SAT technology. (Joint work with Warren Hunt and Nathan Wetzler)