Title: Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs
Language: English
Authors: Altmanninger, Johannes 
Rebola Pardo, Adrian 
Issue Date: 2020
Citation: 
Altmanninger, J., & Rebola Pardo, A. (2020). Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs. In CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20–21, 2020, New Orleans, LA, USA / Blanchette, Jasmin; Hriţcu, Cătălin. ACM. https://doi.org/10.1145/3372885.3373821
Abstract: 
The clausal proof format DRAT is the standard de facto to certify SAT solvers' unsatisfiability results. DRAT proofs act as logs of clause inferences and clause deletions in the solver. The non-monotonic nature of the proof system makes deletions relevant. State-of-the-art proof checkers ignore deletions of unit clauses, differing from the standard in meaningful ways that require adaptions when proofs are generated or used for purposes other than checking. On the other hand, dealing with unit deletions in the proof checker breaks many of the usual invariants used for efficiency reasons. Furthermore, many SAT solvers introduce spurious unit deletions in proofs. These deletions are never intended to be applied in the checker but are nevertheless introduced, making many proofs generated by state-of-the-art solvers incorrect. We present the first competitive DRAT checker that honors unit deletions, as well as fixes for the spurious deletion issue in proof generation. Our experimental results confirm that unit deletions can be applied with similar average performance to state-of-the-art checkers. We also confirm that a large fraction of the proofs generated during the last SAT solving competition do not respect the DRAT standard. This result was confirmed with proof incorrectness certificates that were independently validated. We find that our proof incorrectness certificates can be of help when debugging SAT solvers and DRAT checkers.
Keywords: DRAT proofs; DRAT checking; SAT solving
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-8431
http://hdl.handle.net/20.500.12708/802
Library ID: AC15574175
ISBN: 9781450370974
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Inproceedings
Konferenzbeitrag
Appears in Collections:Conference Paper

Files in this item:



Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.

Page view(s)

96
checked on Jun 19, 2022

Download(s)

191
checked on Jun 19, 2022

Google ScholarTM

Check