Solving Boolean satisfiability using local search guided by unit clause elimination

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.