[Back]

W. Forkel, T. Philipp, A. Rebola Pardo, E. Werner:
"Fuzzing and Verifying RAT Refutations with Deletion Information";
in: "Florida Artificial Intelligence Research Society Conference", AAAI Press, 2017, 190 - 193.

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.

Project Head Georg Weissenbacher:
Bit-level Accurate Reasoning and Interpolation