|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.
|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
|Appears in Collections:||Beitrag in Konferenzband | Conference Paper|
Show full item record
Files in this item:
|Frying the Egg Roasting the Chicken Unit Deletions in DRAT Proofs.pdf||736.98 kB||Adobe PDF||View/Open|
checked on Sep 1, 2020
checked on Sep 1, 2020
Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.