Algorithm Engineering and Experiments
Algorithm Engineering and Experiments
复制标题
算法工程与实验
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
C. Stein
中科院分区：
文献类型：
--
作者：
D. Mount;C. Stein
布尔可满足性（SAT）的主要算法是基于搜索空间的深度优先树遍历（DLL过程[6]）或分辨率（DP过程[7]）。在这项工作中，我们引入了一个变种的广度优先搜索（BFS）的基础上的能力，零抑制二进制决策图（ZDD）competencies表示稀疏或结构化的子集集合。虽然BFS可能需要指数数量的内存，我们的新算法执行BFS直接与隐式表示，并实现非常规的减少搜索空间。我们经验性地评估我们的实现经典SAT实例难以DLL/DP求解器。我们的主要结果是经验Θ n4运行时的洞-n实例，DLL求解器需要指数时间。
Leading algorithms for Boolean satisfiability (SAT) are based on either a depth-first tree traversal of the search space (the DLL procedure [6]) or resolution (the DP procedure [7]). In this work we introduce a variant of BreadthFirst Search (BFS) based on the ability of Zero-Suppressed Binary Decision Diagrams (ZDDs) to compactly represent sparse or structured collections of subsets. While a BFS may require an exponential amount of memory, our new algorithm performs BFS directly with an implicit representation and achieves unconventional reductions in the search space. We empirically evaluate our implementation on classical SAT instances difficult for DLL/DP solvers. Our main result is the empirical Θ n4 runtime for hole-n instances, on which DLL solvers require exponential time.