z-logo
open-access-imgOpen Access
Two flavors of DRAT
Author(s) -
Adrian Rebola Pardo,
Armin Biere
Publication year - 2019
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/lt8r
Subject(s) - mathematical proof , computer science , class (philosophy) , state (computer science) , de facto , theoretical computer science , mathematics , algorithm , artificial intelligence , law , political science , geometry
DRAT proofs have become the de facto standard for certifying SAT solvers’ results. State-of-the-art DRAT checkers are able to efficiently establish the unsatisfiability of a formula. However, DRAT checking requires unit propagation, and so it is computationally non-trivial. Due to design decisions in the development of early DRAT checkers, the class of proofs accepted by state-of-the-art DRAT checkers differs from the class of proofs accepted by the original definition. In this paper, we formalize the operational definition of DRAT proofs, and discuss practical implications of this difference for generating as well as checking DRAT proofs. We also show that these theoretical differences have the potential to affect whether some proofs generated in practice by SAT solvers are correct or not.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.
Having issues? You can contact us here