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

Abstract

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
PublisherIEEE
Publication date7. Jan 2019
Pages197-205
ISBN (Print)978-1-5386-7567-0
ISBN (Electronic)978-0-9835678-8-2
DOIs
Publication statusPublished - 7. Jan 2019
EventFormal Methods in Computer-Aided Design - Austin, United States
Duration: 30. Oct 20182. Nov 2018

Conference

ConferenceFormal Methods in Computer-Aided Design
CountryUnited States
CityAustin
Period30/10/201802/11/2018

Cite this

Rebola-Pardo, A., & Cruz-Filipe, L. (2019). Complete and Efficient DRAT Proof Checking. In N. Bjørner, & A. Gurfinkel (Eds.), Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018 (pp. 197-205). IEEE. https://doi.org/10.23919/FMCAD.2018.8602993