Fuzzing and verifying RAT refutations with deletion information

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung



Contemporary SAT solvers emit proofs of unsatisfiability in the DRAT format to guarantee correctness of their answers. Therefore, correctness of SAT solvers is reduced to correctness of DRAT checkers, which are relatively small programs that decide whether a DRAT refutation is correct. We present a new fuzzing technique that automatically finds bugs in DRAT checkers by comparing the outputs of two DRAT checkers. In case their outputs are different a mechanically verified DRAT checker finally decides which checker has given the correct answer. Experiments show that our method finds bugs in available checkers, and also demonstrate that a common design choice in efficient DRAT checkers is inconsistent with the specification.


TitelFLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference
Herausgeber (Verlag)AAAI Press
ISBN (elektronisch)978-157735787-2
PublikationsstatusVeröffentlicht - 2017

Externe IDs

Scopus 85029531980