Complete and Efficient DRAT Proof Checking

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

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer 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.

OriginalsprogEngelsk
TitelProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
RedaktørerNikolaj Bjørner, Arie Gurfinkel
ForlagIEEE
Publikationsdato7. jan. 2019
Sider197-205
ISBN (Trykt)978-1-5386-7567-0
ISBN (Elektronisk)978-0-9835678-8-2
DOI
StatusUdgivet - 7. jan. 2019
BegivenhedFormal Methods in Computer-Aided Design - Austin, USA
Varighed: 30. okt. 20182. nov. 2018

Konference

KonferenceFormal Methods in Computer-Aided Design
Land/OmrådeUSA
ByAustin
Periode30/10/201802/11/2018

Fingeraftryk

Dyk ned i forskningsemnerne om 'Complete and Efficient DRAT Proof Checking'. Sammen danner de et unikt fingeraftryk.

Citationsformater