Complete and Efficient DRAT Proof Checking

Adrián Rebola-Pardo, Luís Cruz-Filipe

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


DRAT proofs have become the standard for verifying unsatisfiability proofs emitted by modern SAT solvers. However, recent work showed that the specification of the format differs from its implementation in existing tools due to optimizations necessary for efficiency. Although such differences do not compromise soundness of DRAT checkers, the sets of correct proofs according to the specification and to the implementation are incomparable. We discuss how it is possible to design DRAT checkers faithful to the specification by carefully modifying the standard optimization techniques. We implemented such modifications in a configurable DRAT checker. Our experimental results show negligible overhead due to these modifications, suggesting that efficient verification of the DRAT specification is possible. Furthermore, we show that the differences between specification and implementation of DRAT often arise in practice.

Original languageEnglish
Title of host publicationProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
EditorsNikolaj Bjørner, Arie Gurfinkel
Publication date7. Jan 2019
ISBN (Print)978-1-5386-7567-0
ISBN (Electronic)978-0-9835678-8-2
Publication statusPublished - 7. Jan 2019
EventFormal Methods in Computer-Aided Design - Austin, United States
Duration: 30. Oct 20182. Nov 2018


ConferenceFormal Methods in Computer-Aided Design
Country/TerritoryUnited States


Dive into the research topics of 'Complete and Efficient DRAT Proof Checking'. Together they form a unique fingerprint.

Cite this