A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

被引：26
作者：
Blanchette, Jasmin Christian [1 ,2 ]
Fleury, Mathias [2 ,3 ]
Lammich, Peter [4 ]
Weidenbach, Christoph [2 ]
机构：
[1] Vrije Univ Amsterdam, Dept Comp Sci, Sect Theoret Comp Sci, De Boelelaan 1081a, NL-1081 HV Amsterdam, Netherlands
[2] Max Planck Inst Informat, Saarland Informat Campus E1 4, D-66123 Saarbrucken, Germany
[3] Saarbrucken Grad Sch Comp Sci, Saarland Informat Campus E1 3, D-66123 Saarbrucken, Germany
[4] Tech Univ Munich, Inst Informat, Boltzmannstr 3, Garching, Germany
来源：
JOURNAL OF AUTOMATED REASONING | 2018年 / 61卷 / 1-4期
基金：
欧洲研究理事会;
关键词：
SAT solvers; CDCL; DPLL; Proof assistants; Isabelle/HOL; MODULO THEORIES; VERIFICATION; SATISFIABILITY; ISABELLE/HOL; PROGRAM; LOCALES; LOGIC; DPLL;
D O I：
10.1007/s10817-018-9455-7
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We developed a formal framework for conflict-driven clause learning (CDCL) using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL calculus is connected first to a more concrete calculus, then to a SAT solver expressed in a functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland (DPLL) calculus. The imperative program relies on the two-watched-literal data structure and other optimizations found in modern solvers. We used Isabelle's Refinement Framework to automate the most tedious refinement steps. The most noteworthy aspects of our work are the inclusion of rules for forget, restart, and incremental solving and the application of stepwise refinement.
引用
收藏
页码：333 / 365
页数：33
相关论文
共 60 条
  • [1] [Anonymous], 2019, LCP ISABELLE 2019
  • [2] [Anonymous], 2012, IWIL 2010 EPIC
  • [3] [Anonymous], CAMBRIDGE TRACTS THE
  • [4] [Anonymous], 2014, Concrete Semantics: With Isabelle/HOL
  • [5] [Anonymous], 1940, J. Symb. Log., DOI DOI 10.2307/2266170
  • [6] Bachmair L., 2001, HDB AUTOMATED REASON, V1, P19, DOI DOI 10.1016/B978-044450813-3/50004-7
  • [7] Locales: A Module System for Mathematical Theories
    Ballarin, Clemens
    [J]. JOURNAL OF AUTOMATED REASONING, 2014, 52 (02) : 123 - 153
  • [8] Bayardo R. J. Jr., 1996, Principles and Practice of Constraint Programming - CP96. Second International Conference - CP96. Proceedings, P46
  • [9] Becker H., IsaFoL: Isabelle formalization of logic
  • [10] Biere A, 2015, LNCS, V5584, P237
123456