Satisfiability Checking: Theory and Applications

摘要

Satisfiability checking aims to develop algorithms and tools for checking the satisfiability of existentially quantified logical formulas. Besides powerful SAT solvers for solving prepositional logic formulas, sophisticated SAT-modulo-theories (SMT) solvers are available for a wide range of theories, and are applied as black-box engines for many techniques in different areas. In this paper we give a short introduction to the theoretical foundations of satisfiability checking, mention some of the most popular tools, and discuss the successful embedding of SMT solvers in different technologies.