Verifying the DPLL Algorithm in Dafny

TL;DR

This paper presents a verified implementation of a SAT solver in Dafny, addressing the challenge of ensuring correctness in complex, high-performance algorithms where traditional certificates are hard to verify.

Contribution

The paper introduces a formally verified SAT solver in Dafny, providing a trustworthy alternative to traditional high-performance solvers with complex code.

Findings

Verified SAT solver implementation in Dafny

Addresses correctness verification of complex algorithms

Enhances trustworthiness of SAT solving processes

Abstract

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.