A two-phase algorithm for solving a class of hard satisfiability problems
A two-phase algorithm for solving a class of hard satisfiability problems
复制标题
DOI：
10.1016/s0167-6377(98)00052-2
复制
发表时间：
1998-10-01
影响因子：
1.1
通讯作者：
van Maaren, H
中科院分区：
文献类型：
--
作者：
Warners, JP;van Maaren, H
DIMACS可满足性（SAT）基准测试套件包含一组对于现有算法来说非常困难的实例。这些实例是从学习32位上的奇偶校验函数中产生的。在本文中，我们开发了一个两阶段的算法，能够解决这些情况。在第一阶段，一个多项式可解的子问题被确定和解决。使用这个问题的解决方案，我们可以大大限制搜索空间的大小在第二阶段的算法，这是一个著名的Davis-Putnam-Logemann-loveland算法的扩展。最后，我们报告我们的计算结果的奇偶校验实例。(C)1998 Elsevier Science B. V.保留所有权利。
The DIMACS suite of satisfiability (SAT) benchmarks contains a set of instances that are very hard for existing algorithms. These instances arise from learning the parity function on 32 bits. In this paper we develop a two-phase algorithm that is capable of solving these instances. In the first phase, a polynomially solvable subproblem is identified and solved. Using the solution to this problem, we can considerably restrict the size of the search space in the second phase of the algorithm, which is an extension of the well-known Davis-Putnam-Logemann-loveland algorithm. We conclude with reporting on our computational results on the parity instances. (C) 1998 Elsevier Science B.V. All rights reserved.