Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking
Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking
复制标题
通过经过验证的 SAT 验证检查获得工业强度认证的 SAT 解决方案
DOI：
10.1007/978-3-642-14808-8_18
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Joao Marques
中科院分区：
文献类型：
--
作者：
A. Darbari;B. Fischer;Joao Marques
布尔值满意度（SAT）求解器现在通常用于验证大型工业问题。但是，它们在铁路，航空电子和汽车行业等安全 - 关键领域中的应用需要对结果进行某种形式的保证，因为求解器可以（有时甚至是）有错误。不幸的是，现代且高度优化的SAT求解器的复杂性使得其正确性的直接正式证明不切实际。本文提出了一种替代方法，将不受信任的工业强度，SAT求解器插入一个受信任的，正式验证的SAT证券检查器中，以提供工业强度的认证SAT解决方案。我们方法的关键特征是（i）Checker与特定的SAT求解器无关，而是证明任何尊重约定格式的求解器，以满足和不可信性的要求，（ii）Checker会自动从正式开发中提取和（iii）组合系统可以用作独立的可执行程序，而不是任何支持定理供体。系统的核心是在COQ中正式设计和验证的不可信性索赔的检查程序。我们介绍其正式设计并概述正确性标准。实际的独立检查器自动从COQ开发中提取。对Checker对SAT竞赛竞赛的代表性工业基准的评估表明，尽管它比未经未经认证的SAT检查员慢，但它比在交互式定理供您使用的基础上实现的认证检查员要快得多。
Boolean Satisfiability (SAT) solvers are now routinely used in the verification of large industrial problems. However, their application in safety-critical domains such as the railways, avionics, and automotive industries requires some form of assurance for the results, as the solvers can (and sometimes do) have bugs. Unfortunately, the complexity of modern and highly optimized SAT solvers renders impractical the development of direct formal proofs of their correctness. This paper presents an alternative approach where an untrusted, industrial-strength, SAT solver is plugged into a trusted, formally verified, SAT proof checker to provide industrial-strength certified SAT solving. The key characteristics of our approach are (i) that the checker is not tied to a specific SAT solver but certifies any solver respecting the agreed format for satisfiability and unsatisfiability claims, (ii) that the checker is automatically extracted from the formal development, and (iii) that the combined system can be used as a standalone executable program independent of any supporting theorem prover. The core of the system is a checker for unsatisfiability claims that is formally designed and verified in Coq. We present its formal design and outline the correctness criteria. The actual standalone checker is automatically extracted from the the Coq development. An evaluation of the checker on a representative set of industrial benchmarks from the SAT Race Competition shows that, albeit it is slower than uncertified SAT checkers, it is significantly faster than certified checkers implemented on top of an interactive theorem prover.