cl-banner

Beyond DRAT: Challenges in Certifying UNSAT

Bertram Felgenhauer

Proceedings of the 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2017), EPiC Series in Computing 51, pp. 46 – 50, 2017.

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.

 

  PDF |    doi:10.29007/2b78

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
}
Nach oben scrollen