Verification of a DPLL Transition System in Rocq
A formal verification of an abstract transition-system presentation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure in the Rocq proof assistant establishes correctness and completeness with respect to satisfiability, and proves termination by showing that the transition relation is well-founded.