Результаты исследований: Научные публикации в периодических изданиях › статья › Рецензирование
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 |
ID: 49829890