Abstract

Contemporary SAT solvers are complex tools and may contain bugs. In order to increase the trust in the results of SAT solving, SAT solvers may produce certificates that can be checked independently. For unsatisfiability certificates, DRAT is the de facto standard. As long as the checkers are not formalized, extending the certificate format would decrease the trust in the checker because its code complexity increases. With the advent of formally verified checkers for DRAT proofs, this is no longer the case. In this note I argue that symmetry breaking is not adequately supported by DRAT proofs, and propose to have dedicated certification for symmetry breaking instead.

BibTeX

@inproceedings{BF-ARCADE17,
 author    = "Bertram Felgenhauer",
 title     = "Beyond DRAT: Challenges in Certifying UNSAT",
 booktitle = "Proceedings of the 1st International Workshop on Automated
              Reasoning: Challenges, Applications, Directions, Exemplary
              Achievements",
 editor    = "Giles Reger and Dmitriy Traytel",
 series    = "EPiC Series in Computing",
 volume    = 51,
 pages     = "46--50",
 year      = 2017
}