A verified SAT solver framework with learn, forget, restart, and incrementality.

摘要

SAT solvers are automatic decision procedures for the propositional satisfiability problem; they play an important role in planning, scheduling, optimization, and especially the formal verification of hardware and software systems. Thus, verifying the correctness of SAT solvers and deriving provably correct solvers has become of major interest. This paper contributes a formal framework for the theory of conflict-driven clause learning (CDCL) underlying modern SAT solvers. The theory is elaborated with the Isabelle/HOL proof assistant, and an abstract algorithm in the form of a state transition system is formulated and verified. By a sequence of refinements, the algorithm is concretized and various optimizations are incorporated; the Isabelle code generator translates the resulting functional algorithm into actually executable code. Finally, an imperative implementation is derived that makes use of efficient mutable data structures, yielding a reasonably efficient and provably correct SAT solver.