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.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming - CP 2001 - 7th International Conference, CP 2001, Proceedings
EditorsToby Walsh
PublisherSpringer Nature
Pages605-609
Number of pages5
ISBN (Print)3540428631, 9783540428633
StatePublished - 1 Jan 2001
Event7th International Conference on Principles and Practice of Constraint Programming, CP 2001 - Paphos, Cyprus
Duration: 26 Nov 20011 Dec 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2239
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Conference on Principles and Practice of Constraint Programming, CP 2001
Country/TerritoryCyprus
CityPaphos
Period26/11/011/12/01

    Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

    Research areas

  • Boolean satisfiability, Empirical evaluation, Local search

ID: 49829404