Lecture Notes in Computer Science, 2001, Volume 2239/2001, 605-609, DOI: 10.1007/3-540-45578-7_48

Solving Boolean Satisfiability Using Local Search Guided by Unit Clause Elimination

Edward A. Hirsch and Arist Kojevnikov

View Related Documents

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

Fulltext Preview

Image of the first page of the fulltext document