Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Solving Boolean Satisfiability Using Local Search Guided by Unit Clause Elimination

Hirsch Edward A. Contact Information and Arist KojevnikovContact Information

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

Contact Information Hirsch Edward A.

URL: http://logic.pdmi.ras.ru/~hirsch

Contact Information Arist Kojevnikov

URL: http://logic.pdmi.ras.ru/~arist
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.105 • Server: mpweb03
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)