Verification of a DPLL Transition System in Rocq
Logic in Computer Science
Summary
The authors provide a formal proof that a simplified version of the DPLL algorithm, used for solving logical puzzles called SAT problems, works correctly and always finishes. They do this by defining the rules the algorithm follows and proving important properties like correctness, completeness, and termination. They also extend the original rules by adding the pure literal rule and show how different strategies can be used to create guaranteed-to-finish solvers. Finally, they implement one such strategy in the Rocq proof assistant and prove it meets the required conditions.
Authors
Julia Dijkstra, Benedikt Ahrens
Abstract
We present 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. We formalize the syntax and semantics of propositional formulas, define the classical and base DPLL transition systems, and prove 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, we introduce an abstract notion of strategy and derive a terminating solver from any strategy satisfying suitable conditions. We then implement a concrete strategy in Rocq and show that it satisfies the strategy specification.