Conflict-driven clause learning SAT solvers

Joao Marques-Silva, Ines Lynce, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingChapter

199 Scopus citations

Abstract

One of the most important paradigm shifts in the use of SAT solvers for solving industrial problems has been the introduction of clause learning. Clause learning entails adding a new clause for each conflict during backtrack search. This new clause prevents the same conflict from occurring again during the search process. Moreover, sophisticated techniques such as the identification of unique implication points in a graph of implications, allow creating clauses that more precisely identify the assignments responsible for conflicts. Learned clauses often have a large number of literals. As a result, another paradigm shift has been the development of new data structures, namely lazy data structures, which are particularly effective at handling large clauses. These data structures are called lazy due to being in general unable to provide the actual status of a clause. Efficiency concerns and the use of lazy data structures motivated the introduction of dynamic heuristics that do not require knowing the precise status of clauses. This chapter describes the ingredients of conflict-driven clause learning SAT solvers, namely conflict analysis, lazy data structures, search restarts, conflict-driven heuristics and clause deletion strategies.

Original languageEnglish (US)
Title of host publicationHandbook of Satisfiability
PublisherIOS Press
Pages131-153
Number of pages23
Edition1
ISBN (Print)9781586039295
DOIs
StatePublished - Jan 1 2009

Publication series

NameFrontiers in Artificial Intelligence and Applications
Number1
Volume185
ISSN (Print)0922-6389

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Conflict-driven clause learning SAT solvers'. Together they form a unique fingerprint.

Cite this