Boolean satisfiability from theoretical hardness to practical success

Sharad Malik, Lintao Zhang
[doi] [Google Scholar] [DBLP] [Citeseer] [url]
Read: 09 July 2020

Communications of the ACM 52(8)
Association for Computing Machinery
New York, NY, USA
Pages 76-82
August 2009
Note(s): SAT solver, SMT solver, survey
Papers: demoura:cacm:2011

This paper is a great intro/overview of SAT solving: what it is, why it is (NP) hard, how SAT solvers work, the role of benchmarks and competitions, the massive performance improvements in the 10 years prior to it being published and the industrial impact.

Worth reading in conjunction with the SMT intro/overview in demoura:cacm:2011.

SAT solver