Chapter 4: Conflict-driven clause learning SAT solvers

Joao Marques-Silva, Ines Lynce, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingChapter

30 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
Subtitle of host publicationSecond Edition. Part 1/Part 2
EditorsArmin Biere, Marijn Heule, Hans Van Maaren, Toby Walsh
PublisherIOS Press BV
Pages133-182
Number of pages50
ISBN (Electronic)9781643681603
DOIs
StatePublished - 2021

Publication series

NameFrontiers in Artificial Intelligence and Applications
Volume336
ISSN (Print)0922-6389
ISSN (Electronic)1879-8314

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence

Fingerprint

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

Cite this