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

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Konferenceartikel › Forskning › 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.

Originalsprog	Engelsk
Tidsskrift	Lecture Notes in Computer Science
Vol/bind	10395
Sider (fra-til)	220-236
Antal sider	17
DOI	https://doi.org/10.1007/978-3-319-63046-5_14
Status	Udgivet - 11 jul. 2017
Udgivet eksternt	Ja
Begivenhed	Conference on Automated Deduction - Lindholmen Conference Centre, Göteborg, Sverige Varighed: 6 aug. 2017 → 11 aug. 2017 Konferencens nummer: 26 https://www.lindholmen.se/en/event/international-conference-automated-deduction-cade-26

Konference

Konference	Conference on Automated Deduction
Nummer	26
Lokation	Lindholmen Conference Centre
Land/Område	Sverige
By	Göteborg
Periode	06/08/2017 → 11/08/2017
Internetadresse	https://www.lindholmen.se/en/event/international-conference-automated-deduction-cade-26

Adgang til dokumentet

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

Citationsformater

@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

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater