Hirsch, E. A., SAT Local Search Algorithms: Worst-Case Study.
Journal of Automated Reasoning (special issue on SAT) 24(1/2): 127-143, February 2000.
Also published in the book "Highlights of Satisfiability Research in the Year 2000",
Volume 63 in Frontiers in Artificial Intelligence and Applications, IOS Press, 2000.

Abstract. 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 important classes of formulas as well as poor performance on some other ones. In contrast, theoretical knowledge of their worst-case behaviour is very limited. However, many worst-case upper and lower bounds of the form 2an (a<1 is a constant) are known for other SAT algorithms, e.g. 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 NP-complete.

Full text (draft): [ .ps.gz (93 Kb) ]

Back to the list of papers