The Mechanical Verification of a DPLL-Based Satisfiability Solver

Abstract

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