Complete and Efficient DRAT Proof Checking

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

doi:10.23919/FMCAD.2018.8602993

Complete and Efficient DRAT Proof Checking

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

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-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 language	English
Title of host publication	Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
Editors	Nikolaj Bjørner, Arie Gurfinkel
Number of pages	9
Place of Publication	United States
Publisher	IEEE
Publication date	7 Jan 2019
Pages	197-205
ISBN (Print)	978-1-5386-7567-0
DOIs	https://doi.org/10.23919/FMCAD.2018.8602993
Publication status	Published - 7 Jan 2019
Externally published	Yes
Event	Formal Methods in Computer Aided Design conference - Austin, United States Duration: 30 Oct 2018 → 2 Nov 2018 Conference number: 18 https://www.cs.utexas.edu/~hunt/FMCAD/FMCAD18/

Conference

Conference	Formal Methods in Computer Aided Design conference
Number	18
Country/Territory	United States
City	Austin
Period	30/10/2018 → 02/11/2018
Internet address	https://www.cs.utexas.edu/~hunt/FMCAD/FMCAD18/

Keywords

DRAT
proof checking
unsatisfiability proofs
SAT solving
formal verification

Access to Document

10.23919/FMCAD.2018.8602993

Cite this

@inproceedings{a927927f722d40ecaacad5dbba4d489a,

title = "Complete and Efficient DRAT Proof Checking",

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.",

keywords = "DRAT, proof checking, unsatisfiability proofs, SAT solving, formal verification",

author = "Adri{\'a}n Rebola-Pardo and Lu{\'i}s Cruz-Filipe",

year = "2019",

month = jan,

day = "7",

doi = "10.23919/FMCAD.2018.8602993",

language = "English",

isbn = "978-1-5386-7567-0",

pages = "197--205",

editor = "Nikolaj Bj{\o}rner and Arie Gurfinkel",

booktitle = "Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018",

publisher = "IEEE",

address = "United States",

note = "Formal Methods in Computer Aided Design conference, FMCAD ; Conference date: 30-10-2018 Through 02-11-2018",

url = "https://www.cs.utexas.edu/\textasciitilde{}hunt/FMCAD/FMCAD18/",

}

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. IEEE, United States, pp. 197-205, Formal Methods in Computer Aided Design conference, Austin, Texas, United States, 30/10/2018. https://doi.org/10.23919/FMCAD.2018.8602993

Complete and Efficient DRAT Proof Checking. / Rebola-Pardo, Adrián; Cruz-Filipe, Luís.
Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018. ed. / Nikolaj Bjørner; Arie Gurfinkel. United States: IEEE, 2019. p. 197-205.

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Complete and Efficient DRAT Proof Checking

AU - Rebola-Pardo, Adrián

AU - Cruz-Filipe, Luís

N1 - Conference code: 18

PY - 2019/1/7

Y1 - 2019/1/7

N2 - 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.

AB - 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.

KW - DRAT

KW - proof checking

KW - unsatisfiability proofs

KW - SAT solving

KW - formal verification

U2 - 10.23919/FMCAD.2018.8602993

DO - 10.23919/FMCAD.2018.8602993

M3 - Article in proceedings

SN - 978-1-5386-7567-0

SP - 197

EP - 205

BT - Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018

A2 - Bjørner, Nikolaj

A2 - Gurfinkel, Arie

PB - IEEE

CY - United States

T2 - Formal Methods in Computer Aided Design conference

Y2 - 30 October 2018 through 2 November 2018

ER -

Complete and Efficient DRAT Proof Checking

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this