Algorithms for SAT Based on Search in Hamming Balls
Algorithms for SAT Based on Search in Hamming Balls
复制标题
基于汉明球搜索的 SAT 算法
DOI：
10.1007/978-3-540-24749-4_13
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
A. Wolpert
中科院分区：
文献类型：
--
作者：
E. Dantsin;E. Hirsch;A. Wolpert
我们提出了两个简单的算法SAT和证明上界的运行时间。给定一个合取范式的布尔公式F，第一个算法通过重复以下步骤找到F的满意赋值（如果有的话）：随机选择一个赋值A，然后在A周围的汉明球（球的半径取决于F）内搜索一个满意赋值。我们证明，该算法最多只需2个\（^{n - 0.712\sqrt{n}}\）步骤即可求解SAT，错误概率很小，其中n是F中的变量数量。为了去随机化这个算法，我们使用覆盖码而不是随机分配。确定性算法在最多2\（^{n - 2\sqrt{n/log_2n}}\）步中求解SAT。据我们所知，这是第一个非平凡的限制，一个确定性的SAT算法没有限制条款的长度。
We present two simple algorithms for SAT and prove upper bounds on their running time. Given a Boolean formula F in conjunctive normal form, the first algorithm finds a satisfying assignment for F (if any) by repeating the following: Choose an assignment A at random and search for a satisfying assignment inside a Hamming ball around A (the radius of the ball depends on F). We show that this algorithm solves SAT with a small probability of error in at most 2\(^{n - 0.712\sqrt{n}}\) steps, where n is the number of variables in F. To derandomize this algorithm, we use covering codes instead of random assignments. The deterministic algorithm solves SAT in at most 2\(^{n - 2\sqrt{n/log_2n}}\) steps. To the best of our knowledge, this is the first non-trivial bound for a deterministic SAT algorithm with no restriction on clause length.