Verification of a DPLL Transition System in Rocq
J.M. Dijkstra (TU Delft - Electrical Engineering, Mathematics and Computer Science)
B.P. Ahrens – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
S. Dumančić – Graduation committee member (TU Delft - Electrical Engineering, Mathematics and Computer Science)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
This thesis presents a formal verification of an abstract transition-system presentation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure in the Rocq proof assistant. Following Nieuwenhuis et al., SAT solving is modeled as a set of rule-based transitions between states rather than as a concrete algorithm. The thesis formalizes the syntax and semantics of propositional formulas, defines the classical and base DPLL transition systems, and proves their key metatheoretic properties. In particular, we establish correctness and completeness with respect to satisfiability, and we prove termination by showing that the transition relation is well-founded. The formalization extends the original abstract system by also including the pure literal rule. Building on the verified transition system, the thesis introduces an abstract notion of strategy and derives a terminating solver from any strategy satisfying suitable conditions. A concrete strategy is then implemented in Rocq using Equations and shown to satisfy the strategy specification. Together, these results provide a machine-checked and trustworthy core for SAT solving in Rocq and a basis for future extensions toward more advanced systems such as CDCL and DPLL(T).
https://github.com/Vlamonster/RocqSAT
Repository hosting the formalization.
https://vlamonster.github.io/RocqSAT/toc
Documentation of the formalization.