Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Easy Generation and Efficient Verification of Unsatisfiability Proofs

Speaker  Marijn Heule

Affiliation  University of Texas, Austin

Host  Leonardo de Moura

Duration  01:37:32

Date recorded  28 October 2013

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)

©2013 Microsoft Corporation. All rights reserved.
> Easy Generation and Efficient Verification of Unsatisfiability Proofs