An extensible SAT-solver
An extensible SAT-solver
复制标题
DOI：
10.1007/978-3-540-24605-3_37
复制
发表时间：
2004-01-01
期刊：
影响因子：
--
通讯作者：
Sörensson, N
中科院分区：
文献类型：
--
作者：
Eén, N;Sörensson, N
在这篇文章中，我们提出了一个小型的，完整的，高效的冲突驱动学习风格的SAT解算器，如Chaff所示。我们的目标是提供足够的实现细节，使读者能够在很短的时间内构建他或她自己的解算器。这将允许SAT解算器的用户对当前最先进的SAT技术进行特定领域的扩展或改编，以满足特定应用领域的需要。提出的求解器就是考虑到这一点而设计的，其中包括一种添加任意布尔约束的机制。它还支持通过增量SAT接口高效地解决一系列相关的SAT问题。
In this article, we present a small, complete, and efficient SAT-solver in the style of conflict-driven learning, as exemplified by CHAFF. We aim to give sufficient details about implementation to enable the reader to construct his or her own solver in a very short time. This will allow users of SAT-solvers to make domain specific extensions or adaptions of current state-of-the-art SAT-techniques, to meet the needs of a particular application area. The presented solver is designed with this in mind, and includes among other things a mechanism for adding arbitrary boolean constraints. It also supports solving a series of related SAT-problems efficiently by an incremental SAT-interface.