Propositional SAT solving

Joao Marques-Silva, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingChapter

8 Scopus citations

Abstract

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 languageEnglish (US)
Title of host publicationHandbook of Model Checking
PublisherSpringer International Publishing
Pages247-275
Number of pages29
ISBN (Electronic)9783319105758
ISBN (Print)9783319105741
DOIs
StatePublished - May 18 2018

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Mathematics(all)
  • Engineering(all)

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

  • Cite this

    Marques-Silva, J., & Malik, S. (2018). Propositional SAT solving. In Handbook of Model Checking (pp. 247-275). Springer International Publishing. https://doi.org/10.1007/978-3-319-10575-8_9