The Mechanical Verification of a DPLL-Based Satisfiability Solver

被引：19

作者：

Shankar, Natarajan ^{[1
]}

Vaucher, Marc ^{[2
]}

机构：

[1] SRI Int, Comp Sci Lab, Menlo Pk, CA 94025 USA

[2] Ecole Polytech, Palaiseau, France

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2011年 / 269卷

基金：

美国国家科学基金会;

关键词：

SAT solver; backlumping; predicate subtype; dependent type; PVS;

D O I：

10.1016/j.entcs.2011.03.002

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：3 / 17

页数：15

共 20 条

[1]

Boyer R. S., 1984, Automated Theorem Proving : After 25 Years. Proceedings of the Special Session of the 89th Annual Meeting of the American Mathematical Society, P133

[2]

BRYANT RE, 1986, IEEE T COMPUT, V35, P677, DOI 10.1109/TC.1986.1676819

[3]

Clarke EM, 1999, MODEL CHECKING, P1

[4] A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY [J].