Efficient Certified RAT Verification

Luís Cruz-Filipe; Marijn Heule; Warren Hunt Jr; Matt Kaufmann; Peter Schneider-Kamp

doi:10.1007/978-3-319-63046-5_14

Efficient Certified RAT Verification

Luís Cruz-Filipe
, Marijn Heule
, Warren Hunt Jr
, Matt Kaufmann
, Peter Schneider-Kamp

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Abstract

Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive even in highly optimized implementations. We present a new format, called LRAT, which extends the DRAT format with hints that facilitate a simple and fast validation algorithm. Checking validity of LRAT proofs can be implemented using trusted systems such as the languages supported by theorem provers. We demonstrate this by implementing two certified LRAT checkers, one in Coq and one in ACL2.

Original language	English
Journal	Lecture Notes in Computer Science
Volume	10395
Pages (from-to)	220-236
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-319-63046-5_14
Publication status	Published - 11 Jul 2017
Externally published	Yes
Event	Conference on Automated Deduction - Lindholmen Conference Centre, Göteborg, Sweden Duration: 6 Aug 2017 → 11 Aug 2017 Conference number: 26 https://www.lindholmen.se/en/event/international-conference-automated-deduction-cade-26

Conference

Conference	Conference on Automated Deduction
Number	26
Location	Lindholmen Conference Centre
Country/Territory	Sweden
City	Göteborg
Period	06/08/2017 → 11/08/2017
Internet address	https://www.lindholmen.se/en/event/international-conference-automated-deduction-cade-26

Keywords

Clausal proofs
DRAT
LRAT
proof validation
theorem proving

Access to Document

10.1007/978-3-319-63046-5_14

Cite this

@inproceedings{1658ee0c76ab4b199251cbca2477d353,

title = "Efficient Certified RAT Verification",

abstract = "Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive even in highly optimized implementations. We present a new format, called LRAT, which extends the DRAT format with hints that facilitate a simple and fast validation algorithm. Checking validity of LRAT proofs can be implemented using trusted systems such as the languages supported by theorem provers. We demonstrate this by implementing two certified LRAT checkers, one in Coq and one in ACL2.",

keywords = "Clausal proofs, DRAT, LRAT, proof validation, theorem proving",

author = "Lu{\'i}s Cruz-Filipe and Marijn Heule and \{Hunt Jr\}, Warren and Matt Kaufmann and Peter Schneider-Kamp",

note = "26th International Conference on Automated Deduction, CADE 26 ; Conference date: 06-08-2017 Through 11-08-2017; Conference on Automated Deduction, CADE ; Conference date: 06-08-2017 Through 11-08-2017",

year = "2017",

month = jul,

day = "11",

doi = "10.1007/978-3-319-63046-5\_14",

language = "English",

volume = "10395",

pages = "220--236",

journal = "Lecture Notes in Computer Science",

url = "https://www.lindholmen.se/en/event/international-conference-automated-deduction-cade-26",

}

TY - GEN

T1 - Efficient Certified RAT Verification

AU - Cruz-Filipe, Luís

AU - Heule, Marijn

AU - Hunt Jr, Warren

AU - Kaufmann, Matt

AU - Schneider-Kamp, Peter

N1 - Conference code: 26

PY - 2017/7/11

Y1 - 2017/7/11

N2 - Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive even in highly optimized implementations. We present a new format, called LRAT, which extends the DRAT format with hints that facilitate a simple and fast validation algorithm. Checking validity of LRAT proofs can be implemented using trusted systems such as the languages supported by theorem provers. We demonstrate this by implementing two certified LRAT checkers, one in Coq and one in ACL2.

AB - Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive even in highly optimized implementations. We present a new format, called LRAT, which extends the DRAT format with hints that facilitate a simple and fast validation algorithm. Checking validity of LRAT proofs can be implemented using trusted systems such as the languages supported by theorem provers. We demonstrate this by implementing two certified LRAT checkers, one in Coq and one in ACL2.

KW - Clausal proofs

KW - DRAT

KW - LRAT

KW - proof validation

KW - theorem proving

U2 - 10.1007/978-3-319-63046-5_14

DO - 10.1007/978-3-319-63046-5_14

M3 - Conference article

VL - 10395

SP - 220

EP - 236

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - Conference on Automated Deduction

Y2 - 6 August 2017 through 11 August 2017

ER -

Efficient Certified RAT Verification

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this