Preface to special issue on satisfiability modulo theories

Excerpt

Algorithms to determine the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, have become an enabling technology for verification, test-vector generation, compiler optimization, scheduling, and other areas. The development of SMT solvers started in the 90s, with program verification as the main use case, and has seen numerous advances since then, including better methods for Boolean reasoning, more efficient decision procedures for various logical theories, and new approaches to solve formulas with quantifiers. Over the last decade, there has been a consolidation in the way SMT solvers are constructed, with the DPLL(T) architecture having emerged as the standard approach. As a consequence, most solvers today include a CDCL-based SAT solver for efficient Boolean reasoning, augmented with theory-specific decision procedures for theories like linear arithmetic, arrays, or bit-vectors. These ingredients have made SMT techniques well-suited for use in larger automated reasoning and formal verification efforts. …