Practical applications of Boolean Satisfiability

Boolean satisfiability (SAT) solvers have been the subject of remarkable improvements since the mid 90s. One of the main reasons for these improvements has been the wide range of practical applications of SAT. Indeed, examples of modern applications of SAT range from termination analysis in term-rewrite systems to circuit-level prediction of crosstalk noise. The success of SAT solvers motivated many practical applications, but many practical applications have also provided the examples and the challenges that allowed the development of more efficient SAT solvers. This paper provides an overview of some of the most well-known applications of SAT and outlines several other successful applications of SAT. Moreover, the improvements in SAT solvers motivated the development of new algorithms for strategic extensions of SAT. As a result, the paper also provides a brief survey of recent work on extensions of SAT, including pseudo-Boolean constraints, maximum satisfiability, model counting and quantified Boolean formulas.