SAT local search algorithms: Worst-case study
SAT local search algorithms: Worst-case study
复制标题
DOI：
10.1023/a:1006318521185
复制
发表时间：
2000-02-01
期刊：
影响因子：
--
通讯作者：
Hirsch, EA
中科院分区：
文献类型：
--
作者：
Hirsch, EA
最近的实验表明，本地搜索算法（如GSAT）能够找到令人满意的分配许多“硬”布尔公式。对这些算法进行了广泛的实验研究，结果表明，它们在某些重要的公式类上表现良好，而在另一些公式类上表现较差。相比之下，关于它们最坏情况行为的理论知识非常有限。然而，对于其他SAT算法，例如分辨率类算法，已知形式2（alpha n）（alpha < 1是常数）的许多最坏情况的上界和下界。在本文中，我们证明了这种形式的局部搜索算法的上界和下界。我们认为上界的线性尺寸公式的类覆盖了大多数的DIMACS基准，这类公式的可满足性问题是NP-完全的。
Recent experiments demonstrated that local search algorithms (e.g. GSAT) are able to find satisfying assignments for many "hard" Boolean formulas. A wide experimental study of these algorithms demonstrated their good performance on some inportant classes of formulas as well as poor performance on some other ones. In contrast, theoretical knowledge of their worst-case behavior is very limited. However, many worst-case upper and lower bounds of the form 2(alpha n) (alpha < 1 is a constant) are known for other SAT algorithms, for example, resolution-like algorithms. In the present paper we prove both upper and lower bounds of this form for local search algorithms. The class of linear-size formulas we consider for the upper bound covers most of the DIMACS benchmarks; the satisfiability problem for this class of formulas is N P-complete.