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.