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

Department of Mathematics and Computer Science

University of Texas at Austin

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

144 Downloads (Pure)

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
Title of host publication	Automated Deduction - CADE 26 : Proceedings of the 26th International Conference on Automated Deduction
Editors	Leonardo de Moura
Publisher	Springer
Publication date	2017
Pages	220-236
ISBN (Print)	978-3-319-63045-8
ISBN (Electronic)	978-3-319-63046-5
DOIs	https://doi.org/10.1007/978-3-319-63046-5_14
Publication status	Published - 2017
Event	26th International Conference on Automated Deduction - Gothenburg, Sweden Duration: 6. Aug 2017 → 11. Aug 2017 Conference number: 26

Conference

Conference	26th International Conference on Automated Deduction
Number	26
Country/Territory	Sweden
City	Gothenburg
Period	06/08/2017 → 11/08/2017

Series	Lecture Notes in Computer Science
Volume	10395
ISSN	0302-9743

Documents & Links

10.1007/978-3-319-63046-5_14Licence: Unspecified

Efficient Certified RAT VerificationSubmitted manuscript, 165 KB

https://arxiv.org/pdf/1612.02353.pdf

Cite this

@inproceedings{026f0018451448338dc1653b75a36365,

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

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

year = "2017",

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

language = "English",

isbn = "978-3-319-63045-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "220--236",

editor = "{de Moura}, Leonardo",

booktitle = "Automated Deduction - CADE 26",

address = "Germany",

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

}

Cruz-Filipe, L, Heule, M, Hunt, Jr, W, Kaufmann, M & Schneider-Kamp, P 2017, Efficient Certified RAT Verification. in L de Moura (ed.), Automated Deduction - CADE 26: Proceedings of the 26th International Conference on Automated Deduction. Springer, Lecture Notes in Computer Science, vol. 10395, pp. 220-236, 26th International Conference on Automated Deduction, Gothenburg, Sweden, 06/08/2017. https://doi.org/10.1007/978-3-319-63046-5_14

Efficient Certified RAT Verification. / Cruz-Filipe, Luís; Heule, Marijn; Hunt, Jr, Warren et al.

Automated Deduction - CADE 26: Proceedings of the 26th International Conference on Automated Deduction. ed. / Leonardo de Moura. Springer, 2017. p. 220-236 (Lecture Notes in Computer Science, Vol. 10395).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

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

Y1 - 2017

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.

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

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

M3 - Article in proceedings

SN - 978-3-319-63045-8

T3 - Lecture Notes in Computer Science

SP - 220

EP - 236

BT - Automated Deduction - CADE 26

A2 - de Moura, Leonardo

PB - Springer

T2 - 26th International Conference on Automated Deduction

Y2 - 6 August 2017 through 11 August 2017

ER -