摘要翻译：
布尔可满足性(SAT)求解器现在经常用于大型工业问题的验证。然而，它们在铁路、航空电子和汽车工业等安全关键领域的应用需要某种形式的结果保证，因为求解者可能（有时确实）存在缺陷。不幸的是，现代高度优化的SAT求解器的复杂性使得对其正确性的直接形式证明的发展变得不切实际。本文提出了一种替代方法，将一个不可信的、工业强度的SAT求解器插入到一个可信的、正式认证的SAT证明检查器中，以提供工业强度认证的SAT求解。该方法的主要创新和特点是：(i)检查器从形式开发中自动提取；(ii)组合系统可以作为独立于任何支持定理证明器的独立可执行程序；(iii)检查器证明任何SAT求解器关于可满足性和不可满足性声明的约定格式。该系统的核心是一个由COQ正式设计并验证的不可满足性索赔验证器。我们给出了它的形式设计，并概述了正确性证明。实际的独立检查器是从Coq开发中自动提取的。在SAT竞赛的一组具有代表性的工业基准上对认证的checker进行的评估表明，尽管它比未经认证的SAT checker慢，但它比在交互式定理证明器上实现的认证的checker快得多。
---
英文标题：
《Industrial-Strength Formally Certified SAT Solving》
---
作者：
Ashish Darbari and Bernd Fischer and Joao Marques-Silva
---
最新提交年份：
2009
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Logic in Computer Science        计算机科学中的逻辑
分类描述：Covers all aspects of logic in computer science, including finite model theory, logics of programs, modal logic, and program verification. Programming language semantics should have Programming Languages as the primary subject area. Roughly includes material in ACM Subject Classes D.2.4, F.3.1, F.4.0, F.4.1, and F.4.2; some material in F.4.3 (formal languages) may also be appropriate here, although Computational Complexity is typically the more appropriate subject area.
涵盖计算机科学中逻辑的所有方面，包括有限模型理论，程序逻辑，模态逻辑和程序验证。程序设计语言语义学应该把程序设计语言作为主要的学科领域。大致包括ACM学科类D.2.4、F.3.1、F.4.0、F.4.1和F.4.2中的材料；F.4.3（形式语言）中的一些材料在这里也可能是合适的，尽管计算复杂性通常是更合适的主题领域。
--
一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  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, 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 certified, SAT proof checker to provide industrial-strength certified SAT solving. The key novelties and characteristics of our approach are (i) that the checker is automatically extracted from the formal development, (ii), that the combined system can be used as a standalone executable program independent of any supporting theorem prover, and (iii) that the checker certifies any SAT solver respecting the agreed format for satisfiability and unsatisfiability claims. The core of the system is a certified checker for unsatisfiability claims that is formally designed and verified in Coq. We present its formal design and outline the correctness proofs. The actual standalone checker is automatically extracted from the the Coq development. An evaluation of the certified 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.
---
PDF链接：
https://arxiv.org/pdf/0911.1678