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