Write a Blog >>
Mon 20 Jan 2020 12:07 - 12:30 at Maurepas - Automated verification and SAT solving Chair(s): Ori Lahav

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.

Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

11:45 - 12:30
Automated verification and SAT solvingCPP at Maurepas
Chair(s): Ori Lahav Tel Aviv University
11:45
22m
Talk
Verifying x86 Instruction Implementations
CPP
Shilpi Goel Centaur Technology, Inc., Anna Slobodova Centaur Technology, Inc., Rob Sumners Centaur Technology, Inc., Sol Swords Centaur Technology, Inc.
DOI Pre-print File Attached
12:07
22m
Talk
Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs
CPP
DOI Pre-print Media Attached