Solving Boolean Satisfiability Using Local Search Guided by Unit Clause Elimination
Hirsch Edward A. 5
and Arist Kojevnikov6 
| (5) |
Steklov Institute of Mathematics at St.Petersburg, 27 Fontanka, 191011 St.Petersburg, Russia |
| (6) |
Department of Mathematics and Mechanics, St.Petersburg State University, St.Petersburg, Russia |
Abstract
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.
Keywords: Boolean satisfiability - local search - empirical evaluation
Supported by INTAS YSF 99-4044,RFBR 99-01-00113 and RAS Young Scientists Project #1 of the 6th competition (1999).
References secured to subscribers.