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

被引：14

作者：

Blanchette, Jasmin Christian ^{[1
,2
,3
]}

Fleury, Mathias ^{[3
]}

Weidenbach, Christoph ^{[3
]}

机构：

[1] Inria Nancy Grand Est, Villers Les Nancy, France

[2] LORIA, Villers Les Nancy, France

[3] Max Planck Inst Informat, Saarbrucken, Germany

来源：

AUTOMATED REASONING (IJCAR 2016) | 2016年 / 9706卷

关键词：

VERIFICATION; GENERATION; LOCALES;

D O I：

10.1007/978-3-319-40229-1_4

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We developed a formal framework for CDCL (conflict-driven clause learning) in Isabelle/HOL. Through a chain of refinements, an abstract CDCL calculus is connected to a SAT solver expressed in a functional programming language, with total correctness guarantees. The framework offers a convenient way to prove metatheorems and experiment with variants. Compared with earlier SAT solver verifications, the main novelties are the inclusion of rules for forget, restart, and incremental solving and the application of refinement.

引用

页码：25 / 44

页数：20

共 44 条

[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] Locales: A Module System for Mathematical Theories [J].

Ballarin, Clemens .

JOURNAL OF AUTOMATED REASONING, 2014, 52 (02) :123-153

[7]

Bayardo R. J. Jr., 1996, Principles and Practice of Constraint Programming - CP96. Second International Conference - CP96. Proceedings, P46

[8] Bounded model checking [J].

Biere, Armin .

Frontiers in Artificial Intelligence and Applications, 2009, 185 (01) :457-481

[9]

Blanchette J.C, FORMALIZATION WEIDEN

[10]

Blanchette J.C., ISAFOL ISABELLE FORM

← 1 2 3 4 5 →