The quest for efficient boolean satisfiability solvers

Lintao Zhang, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

48 Scopus citations

Abstract

The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enable significant practical applications. Since the first development of the basic search based algorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) about forty years ago, this area has seen active research effort with many interesting contributions that have culminated in state-of-the-art SAT solvers today being able to handle problem instances with thousands, and in same cases even millions, of variables. In this paper we examine some of the main ideas along this passage that have led to our current capabilities. Given the depth of the literature in this field, it is impossible to do this in any comprehensive way; rather we focus on techniques with consistent demonstrated efficiency in available solvers. For the most part, we focus on techniques within the basic DPLL search framework, but also briefly describe other approaches and look at some possible future research directions.

Original languageEnglish (US)
Title of host publicationAutomated Deduction - CADE-18 - 18th International Conference on Automated Deduction, Proceedings
EditorsAndrei Voronkov
PublisherSpringer Verlag
Pages295-313
Number of pages19
ISBN (Print)3540439315, 9783540439318
DOIs
StatePublished - 2002
Event18th International Conference on Automated Deduction, CADE 2002 - Copenhagen, Denmark
Duration: Jul 27 2002Jul 30 2002

Publication series

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

Other

Other18th International Conference on Automated Deduction, CADE 2002
CountryDenmark
CityCopenhagen
Period7/27/027/30/02

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'The quest for efficient boolean satisfiability solvers'. Together they form a unique fingerprint.

  • Cite this

    Zhang, L., & Malik, S. (2002). The quest for efficient boolean satisfiability solvers. In A. Voronkov (Ed.), Automated Deduction - CADE-18 - 18th International Conference on Automated Deduction, Proceedings (pp. 295-313). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2392). Springer Verlag. https://doi.org/10.1007/3-540-45620-1_26