Title: Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs
Language: English
Authors: Altmanninger, Johannes 
Rebola Pardo, Adrian
Keywords: DRAT proofs; DRAT checking; SAT solving
Issue Date: 2020
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.
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 
License URI: http://rightsstatements.org/vocab/InC/1.0/
Publication Type: Inproceedings
Konferenzbeitrag
Appears in Collections:Beitrag in Konferenzband | Conference Paper

Files in this item:

Show full item record

Page view(s)

6
checked on Sep 1, 2020

Download(s)

2
checked on Sep 1, 2020

Google ScholarTM

Check


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