Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
复制标题
DOI：
10.1016/j.tcs.2010.09.014
复制
发表时间：
2010-11-12
影响因子：
1.1
通讯作者：
Maric, Filip
中科院分区：
文献类型：
--
作者：
Maric, Filip
我们提出了一个形式化和正式的全正确性证明系统Isabelle/HOL内的MiniSAT样SAT求解器。求解器是基于DPLL过程，并采用最先进的SAT解决技术，包括冲突引导的回跳，子句学习，和两个观看单元传播计划。一个浅嵌入到Isabelle/HOL的使用和求解器表示为一组递归HOL功能。基于此规范，Isabelle的内置代码生成器可用于生成几种支持的函数式语言（Haskell、SML和OCaml）的可执行代码。据我们所知，以这种方式实现的SAT求解器是第一个完全正式和机械验证的现代SAT求解器。(C)2010 Elsevier B. V.保留所有权利。
We present a formalization and a formal total correctness proof of a MiniSAT-like SAT solver within the system Isabelle/HOL. The solver is based on the DPLL procedure and employs most state-of-the-art SAT solving techniques, including the conflict-guided backjumping, clause learning, and the two-watched unit propagation scheme. A shallow embedding into Isabelle/HOL is used and the solver is expressed as a set of recursive HOL functions. Based on this specification, the Isabelle's built-in code generator can be used to generate executable code in several supported functional languages (Haskell, SML, and OCaml). The SAT solver implemented in this way is, to our knowledge, the first fully formally and mechanically verified modern SAT solver. (C) 2010 Elsevier B.V. All rights reserved.