The Quest for Efficient Boolean Satisfiability Solvers
The Quest for Efficient Boolean Satisfiability Solvers
复制标题
DOI：
10.1007/3-540-45657-0_2
复制
发表时间：
2002-07
期刊：
影响因子：
--
通讯作者：
Lintao Zhang;S. Malik
中科院分区：
文献类型：
--
作者：
Lintao Zhang;S. Malik
布尔可满足性 (SAT) 的经典 NP 完全问题不仅在理论计算机科学界引起了极大的兴趣，而且在该问题的实际解决方案能够实现重要实际应用的领域也引起了极大的兴趣。自从大约 40 年前 Davis、Putnam、Logemann 和 Loveland (DPLL) 首次开发基于基本搜索的算法以来，该领域已经进行了积极的研究工作，并做出了许多有趣的贡献，最终形成了当今最先进的 SAT 求解器，能够处理具有数千个甚至数百万个变量的问题实例。在本文中，我们研究了这段文章中的一些主要思想，这些思想导致了我们目前的能力。鉴于该领域文献的深度，不可能以任何全面的方式做到这一点；相反，我们专注于在可用求解器中具有一致证明效率的技术。在很大程度上，我们关注基本 DPLL 搜索框架内的技术，但也简要描述其他方法并着眼于一些未来可能的研究方向。
The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enable significant practical applications. Since the first development of the basic search based algorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) about forty years ago, this area has seen active research effort with many interesting contributions that have culminated in state-of-the-art SAT solvers today being able to handle problem instances with thousands, and in same cases even millions, of variables. In this paper we examine some of the main ideas along this passage that have led to our current capabilities. Given the depth of the literature in this field, it is impossible to do this in any comprehensive way; rather we focus on techniques with consistent demonstrated efficiency in available solvers. For the most part, we focus on techniques within the basic DPLL search framework, but also briefly describe other approaches and look at some possible future research directions.