Verification of a DPLL Transition System in Rocq

Julia Dijkstra, Benedikt Ahrens

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 Nieuwen…