TY - JOUR

T1 - UnitWalk

T2 - A new SAT solver that uses local search guided by unit clause elimination

AU - Hirsch, Edward A.

AU - Kojevnikov, Arist

PY - 2005/1

Y1 - 2005/1

N2 - In this paper we present a new randomized algorithm for SAT, i.e., the satisfiability problem for Boolean formulas in conjunctive normal form. Despite its simplicity, this algorithm performs well on many common benchmarks ranging from graph coloring problems to microprocessor verification. Our algorithm is inspired by two randomized algorithms having the best current worst-case upper bounds ([27,28] and [30,31]). We combine the main ideas of these algorithms in one algorithm. The two approaches we use are local search (which is used in many SAT algorithms, e.g., in GSAT [34] and WalkSAT [33]) and unit clause elimination (which is rarely used in local search algorithms). In this paper we do not prove any theoretical bounds. However, we present encouraging results of computational experiments comparing several implementations of our algorithm with other SAT solvers. We also prove that our algorithm is probabilistically approximately complete (PAC).

AB - In this paper we present a new randomized algorithm for SAT, i.e., the satisfiability problem for Boolean formulas in conjunctive normal form. Despite its simplicity, this algorithm performs well on many common benchmarks ranging from graph coloring problems to microprocessor verification. Our algorithm is inspired by two randomized algorithms having the best current worst-case upper bounds ([27,28] and [30,31]). We combine the main ideas of these algorithms in one algorithm. The two approaches we use are local search (which is used in many SAT algorithms, e.g., in GSAT [34] and WalkSAT [33]) and unit clause elimination (which is rarely used in local search algorithms). In this paper we do not prove any theoretical bounds. However, we present encouraging results of computational experiments comparing several implementations of our algorithm with other SAT solvers. We also prove that our algorithm is probabilistically approximately complete (PAC).

KW - Boolean satisfiability

KW - empirical evaluation

KW - local search

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

U2 - 10.1007/s10472-005-0421-9

DO - 10.1007/s10472-005-0421-9

M3 - Article

AN - SCOPUS:10344265560

VL - 43

SP - 91

EP - 111

JO - Annals of Mathematics and Artificial Intelligence

JF - Annals of Mathematics and Artificial Intelligence

SN - 1012-2443

IS - 1-4

ER -