This thesis describes CreuSAT, a formally verified SAT solver written in Rust. In addition to implementing the core conflict-driven clause learning (CDCL) algorithm, we also implement a series of crucial optimizations. The most important of these is the two watched literals scheme with blocking literals and circular search, the variable move-to-front (VMTF) decision heuristic, clause deletion, phase saving, and moving average based restarts.
The resulting solver is the first deductively verified solver which is able to consistently solve problems from the SAT competition. This is done while maintaining a relatively small code base, amounting to around 4 thousand lines of proof code and program code combined, with a low proof overhead of around three lines of proof code per line of program code.
In addition to presenting CreuSAT, we also present two other verified SAT solvers. The first of these is called Friday, and represents what we consider to be the minimal verified SAT solver. The second of these is called Robinson, and is a SAT solver based on the Davis–Putnam–Logemann–Loveland (DPLL) algorithm. We present Friday and Robinson mostly for pedagogical reasons, though it should be noted that Robinson is, to the best of our knowledge, the fastest verified DPLL SAT solver presented in literature. To prove the correctness of our solvers, we use the deductive verification tool Creusot, which is based on the WHY3 software verification platform. Creusot leverages the guarantees given by the Rust type system to efficiently translate the program code to a functional program. This results in verification conditions which require little CPU time to prove, and we demonstrate improvements in verification time when compared to other verified solvers.
Our solvers represent the first major usage of Creusot, and the largest published verification effort of Rust code to date. They further mark the first time the direct verification of an imperative program has been able to produce a verified SAT solver capable of solving problems of recent SAT competitions.
| supervisors | Martin Steffen |