Shankar, N., & Vaucher, M. (2011). The mechanical verification of a DPLL-based satisfiability solver. Electronic Notes in Theoretical Computer Science, 269, 3-17.
Recent years have witnessed dramatic improvements in the capabilities of propositional satisfiability procedures or SAT solvers. The speedups are the result of numerous optimizations including conflict-directed backjumping. We use the Prototype Verification System (PVS) to verify a satisfiability procedure based on the Davis–Putnam–Logemann–Loveland (DPLL) scheme that features these optimizations. This exercise is a step toward the verification of an efficient implementation of the satisfiability procedure. Our verification of a SAT solver is part of a larger program of research to provide a secure foundation for inference using a verified reference kernel that contains a verified SAT solver. Our verification exploits predicate subtypes and dependent types in PVS to capture the specification and the key invariants.
Keywords: SAT solver, backlumping, predicate subtype, dependent type, PVS