Easy Generation and Efficient Verification of Unsatisfiability Proofs

We present recent work on validating satisfiability refutations. Satisfiability (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)

Speaker Details

Marijn Heule is a research fellow at the University of Texas at Austin. He received his PhD at Delft University of Technology in the Netherlands in 2008. His research focusses on solving hard combinatorial problems in areas such as formal verification and number theory. Most of his contributions are related to practical Satisfiability solving. He is one of the editors of the Handbook of Satisfiability and an associate editor of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT).

Series:
Microsoft Research Talks
Date:
Speakers:
Marijn Heule
Affiliation:
University of Texas, Austin

Series: Microsoft Research Talks