Propositional SAT solving

Joao Marques-Silva, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingChapter

12 Scopus citations


The Boolean Satisfiability Problem (SAT) is well known in computational complexity, representing the first decision problem to be proved NP-complete. SAT is also often the subject of work in proof complexity. Besides its theoretical interest, SAT finds a wide range of practical applications. Moreover, SAT solvers have been the subject of remarkable efficiency improvements since the mid-1990s, motivating their widespread use in many practical applications including Bounded and Unbounded Model Checking. The success of SAT solvers has also motivated the development of algorithms for natural extensions of SAT, including Quantified Boolean Formulas (QBF), Pseudo-Boolean constraints (PB), Maximum Satisfiability (MaxSAT) and Satisfiability Modulo Theories (SMT) which also see application in the model-checking context. This chapter first covers the organization of modern conflict-driven clause learning (CDCL) SAT solvers, which are used in the vast majority of practical applications of SAT. It then reviews the techniques shown to be effective in modern SAT solvers.

Original languageAmerican English
Title of host publicationHandbook of Model Checking
PublisherSpringer International Publishing
Number of pages29
ISBN (Electronic)9783319105758
ISBN (Print)9783319105741
StatePublished - May 18 2018

ASJC Scopus subject areas

  • General Computer Science
  • General Mathematics
  • General Engineering


Dive into the research topics of 'Propositional SAT solving'. Together they form a unique fingerprint.

Cite this