Efficient Certified RAT Verification

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

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

75 Downloads (Pure)

Resumé

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.
OriginalsprogEngelsk
TitelAutomated Deduction - CADE 26 : Proceedings of the 26th International Conference on Automated Deduction
RedaktørerLeonardo de Moura
ForlagSpringer
Publikationsdato2017
Sider220-236
ISBN (Trykt)978-3-319-63045-8
ISBN (Elektronisk)978-3-319-63046-5
DOI
StatusUdgivet - 2017
Begivenhed26th International Conference on Automated Deduction - Gothenburg, Sverige
Varighed: 6. aug. 201711. aug. 2017
Konferencens nummer: 26

Konference

Konference26th International Conference on Automated Deduction
Nummer26
LandSverige
ByGothenburg
Periode06/08/201711/08/2017
NavnLecture Notes in Computer Science
Vol/bind10395
ISSN0302-9743

Citer dette

Cruz-Filipe, L., Heule, M., Hunt, Jr, W., Kaufmann, M., & Schneider-Kamp, P. (2017). Efficient Certified RAT Verification. I L. de Moura (red.), Automated Deduction - CADE 26: Proceedings of the 26th International Conference on Automated Deduction (s. 220-236). Springer. Lecture Notes in Computer Science, Bind. 10395 https://doi.org/10.1007/978-3-319-63046-5_14
Cruz-Filipe, Luís ; Heule, Marijn ; Hunt, Jr, Warren ; Kaufmann, Matt ; Schneider-Kamp, Peter. / Efficient Certified RAT Verification. Automated Deduction - CADE 26: Proceedings of the 26th International Conference on Automated Deduction. red. / Leonardo de Moura. Springer, 2017. s. 220-236 (Lecture Notes in Computer Science, Bind 10395).
@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",
pages = "220--236",
editor = "{de Moura}, Leonardo",
booktitle = "Automated Deduction - CADE 26",
publisher = "Springer",
address = "Germany",

}

Cruz-Filipe, L, Heule, M, Hunt, Jr, W, Kaufmann, M & Schneider-Kamp, P 2017, Efficient Certified RAT Verification. i L de Moura (red.), Automated Deduction - CADE 26: Proceedings of the 26th International Conference on Automated Deduction. Springer, Lecture Notes in Computer Science, bind 10395, s. 220-236, 26th International Conference on Automated Deduction, Gothenburg, Sverige, 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; Kaufmann, Matt; Schneider-Kamp, Peter.

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

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer 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

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

SP - 220

EP - 236

BT - Automated Deduction - CADE 26

A2 - de Moura, Leonardo

PB - Springer

ER -

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