UnitWalk: A new SAT solver that uses local search guided by unit clause elimination
UnitWalk: A new SAT solver that uses local search guided by unit clause elimination
复制标题
DOI：
10.1007/s10472-005-0421-9
复制
发表时间：
2005-01-01
影响因子：
1.2
通讯作者：
Kojevnikov, A
中科院分区：
文献类型：
--
作者：
Hirsch, EA;Kojevnikov, A
本文提出了一种新的随机化算法，即合取范式中布尔公式的可满足性问题。尽管该算法很简单，但它在从图着色问题到微处理器验证的许多常见基准测试中都表现良好。我们的算法的灵感来自两个具有最佳当前最坏情况上界的随机算法([27，28]和[30，31])。我们将这些算法的主要思想结合在一个算法中。我们使用的两种方法是局部搜索(这在许多SAT算法中使用，例如在GSAT[34]和WalkSAT[33]中)和单位子句消除(这在局部搜索算法中很少使用)。在本文中，我们不证明任何理论界限。然而，我们给出了令人鼓舞的计算实验结果，将我们的算法的几个实现与其他SAT解算器进行了比较。我们还证明了我们的算法是概率近似完全的。
In this paper we present a new randomized algorithm for SAT, i.e., the satisfiability problem for Boolean formulas in conjunctive normal form. Despite its simplicity, this algorithm performs well on many common benchmarks ranging from graph coloring problems to microprocessor verification. Our algorithm is inspired by two randomized algorithms having the best current worst-case upper bounds ([ 27,28] and [ 30,31]). We combine the main ideas of these algorithms in one algorithm. The two approaches we use are local search ( which is used in many SAT algorithms, e.g., in GSAT [34] and WalkSAT [33]) and unit clause elimination ( which is rarely used in local search algorithms). In this paper we do not prove any theoretical bounds. However, we present encouraging results of computational experiments comparing several implementations of our algorithm with other SAT solvers. We also prove that our algorithm is probabilistically approximately complete (PAC).