DOI

Recent experiments demonstrated that local search algorithms (e.g. GSAT) are able to find satisfying assignments for many "hard" Boolean formulas. However, no non-trivial worst-case upper bounds were proved, although many such bounds of the form 2αn (α < 1 is a constant) are known for other SAT algorithms, e.g. resolution-like algorithms. In the present paper we prove such a bound for a local search algorithm, namely for CSAT. The class of formulas we consider covers most of DIMACS benchmarks, the satisfiability problem for this class of formulas is NP-complete.

Язык оригиналаанглийский
Название основной публикацииAlgorithm Theory — SWAT 1998 - 6th Scandinavian Workshop on Algorithm Theory, Proceedings
РедакторыStefan Arnborg, Lars Ivansson
ИздательSpringer Nature
Страницы246-254
Число страниц9
ISBN (печатное издание)3540646825, 9783540646822
DOI
СостояниеОпубликовано - 1 янв 1998
Событие6th Scandinavian Workshop on Algorithm Theory, SWAT 1998 - Stockholm, Швеция
Продолжительность: 8 июл 199810 июл 1998

Серия публикаций

НазваниеLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Том1432
ISSN (печатное издание)0302-9743
ISSN (электронное издание)1611-3349

конференция

конференция6th Scandinavian Workshop on Algorithm Theory, SWAT 1998
Страна/TерриторияШвеция
ГородStockholm
Период8/07/9810/07/98

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

  • Теоретические компьютерные науки
  • Компьютерные науки (все)

ID: 49830053