TY - GEN
T1 - Solving Boolean satisfiability using local search guided by unit clause elimination
AU - Hirsch, Edward A.
AU - Kojevnikov, Arist
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2001.
PY - 2001
Y1 - 2001
N2 - In this paper we present a new randomized algorithm for SAT combining unit clause elimination and local search. The algorithm is inspired by two randomized algorithms having the best current worst-case upper bounds ([9] and [11,12]). Despite its simplicity, our algorithm performs well on many common benchmarks (we present results of its empirical evaluation). It is also probabilistically approximately complete.
AB - In this paper we present a new randomized algorithm for SAT combining unit clause elimination and local search. The algorithm is inspired by two randomized algorithms having the best current worst-case upper bounds ([9] and [11,12]). Despite its simplicity, our algorithm performs well on many common benchmarks (we present results of its empirical evaluation). It is also probabilistically approximately complete.
KW - Boolean satisfiability
KW - Empirical evaluation
KW - Local search
UR - https://www.scopus.com/pages/publications/84947909669
U2 - 10.1007/3-540-45578-7_48
DO - 10.1007/3-540-45578-7_48
M3 - ???researchoutput.researchoutputtypes.contributiontobookanthology.conference???
AN - SCOPUS:84947909669
SN - 3540428631
SN - 9783540428633
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 605
EP - 609
BT - Principles and Practice of Constraint Programming - CP 2001 - 7th International Conference, CP 2001, Proceedings
A2 - Walsh, Toby
T2 - 7th International Conference on Principles and Practice of Constraint Programming, CP 2001
Y2 - 26 November 2001 through 1 December 2001
ER -