Fuzzing and verifying RAT refutations with deletion information
Research output: Contribution to book/conference proceedings/anthology/report › Conference contribution › Contributed › peer-review
Contributors
Abstract
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.
Details
Original language | English |
---|---|
Title of host publication | FLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference |
Publisher | AAAI Press |
Pages | 190-193 |
Number of pages | 4 |
ISBN (electronic) | 978-157735787-2 |
Publication status | Published - 2017 |
Peer-reviewed | Yes |
External IDs
Scopus | 85029531980 |
---|