Standard

SAT local search algorithms : worst-case study. / Hirsch, Edward A.

в: Journal of Automated Reasoning, Том 24, № 1-2, 01.02.2000, стр. 127-143.

Результаты исследований: Научные публикации в периодических изданиях › статья › Рецензирование

Harvard

Hirsch, EA 2000, 'SAT local search algorithms: worst-case study', Journal of Automated Reasoning, Том. 24, № 1-2, стр. 127-143.

APA

Hirsch, E. A. (2000). SAT local search algorithms: worst-case study. Journal of Automated Reasoning, 24(1-2), 127-143.

Vancouver

Hirsch EA. SAT local search algorithms: worst-case study. Journal of Automated Reasoning. 2000 Февр. 1;24(1-2):127-143.

Author

Hirsch, Edward A. / SAT local search algorithms : worst-case study. в: Journal of Automated Reasoning. 2000 ; Том 24, № 1-2. стр. 127-143.

BibTeX

@article{4958cb0a42d549aaa915f6cd88b8eb37,
title = "SAT local search algorithms: worst-case study",
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 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.",
author = "Hirsch, {Edward A.}",
year = "2000",
month = feb,
day = "1",
language = "English",
volume = "24",
pages = "127--143",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Nature",
number = "1-2",

}

RIS

TY - JOUR

T1 - SAT local search algorithms

T2 - worst-case study

AU - Hirsch, Edward A.

PY - 2000/2/1

Y1 - 2000/2/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0034140490&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0034140490

VL - 24

SP - 127

EP - 143

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 1-2

ER -

ID: 49829890