Verifying the DPLL Algorithm in Dafny

Cezar-Constantin Andrici
(Alexandru Ioan Cuza University)
Ştefan Ciobâcă
(Alexandru Ioan Cuza University)

Modern high-performance SAT solvers quickly solve large satisfiability instances that occur in practice. If the instance is satisfiable, then the SAT solver can provide a witness which can be checked independently in the form of a satisfying truth assignment.

However, if the instance is unsatisfiable, the certificates could be exponentially large or the SAT solver might not be able to output certificates. The implementation of the SAT solver should then be trusted not to contain bugs. However, the data structures and algorithms implemented by a typical high-performance SAT solver are complex enough to allow for subtle programming errors.

To counter this issue, we build a verified SAT solver using the Dafny system. We discuss its implementation in the present article.

In Mircea Marin and Adrian Crăciun: Proceedings Third Symposium on Working Formal Methods (FROM 2019), Timişoara, Romania, 3-5 September 2019, Electronic Proceedings in Theoretical Computer Science 303, pp. 3–15.
Published: 2nd September 2019.

ArXived at: http://dx.doi.org/10.4204/EPTCS.303.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org