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 behavior is very limited. However, many worst-case upper and lower bounds of the form 2αn (α < 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 NP-complete.

Язык оригиналаанглийский
Страницы (с-по)127-143
Число страниц17
ЖурналJournal of Automated Reasoning
Том24
Номер выпуска1-2
СостояниеОпубликовано - 1 фев 2000

    Предметные области Scopus

  • Программный продукт
  • Математика и теория расчета
  • Искусственный интеллект

ID: 49829890