Derandomization of Schuler's Algorithm for SAT
Derandomization of Schuler's Algorithm for SAT
复制标题
Schuler SAT 算法的去随机化
DOI：
10.1007/11527695_7
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
A. Wolpert
中科院分区：
文献类型：
--
作者：
E. Dantsin;A. Wolpert
最近 Schuler [17] 提出了一种随机算法，可以在最多 $2^{n(1-1/{\rm log}_{2}(2m))}$ 的预期时间内求解 SAT，最多可达多项式因子，其中 n 和 m 分别是输入公式中变量的数量和子句的数量。这个界限是测试 CNF 中公式可满足性的最著名的上限，对子句长度没有限制（对于 m 与 n 相比不太大的情况）。我们使用基于汉明球搜索的确定性 k-SAT 算法对该算法进行去随机化，并证明我们的确定性算法在运行时间上与 Schuler 的随机算法具有相同的上限。
Recently Schuler [17] presented a randomized algorithm that solves SAT in expected time at most $2^{n(1-1/{\rm log}_{2}(2m))}$ up to a polynomial factor, where n and m are, respectively, the number of variables and the number of clauses in the input formula. This bound is the best known upper bound for testing satisfiability of formulas in CNF with no restriction on clause length (for the case when m is not too large comparing to n). We derandomize this algorithm using deterministic k-SAT algorithms based on search in Hamming balls, and we prove that our deterministic algorithm has the same upper bound on the running time as Schuler’s randomized algorithm.