An Abstract Framework for Satisfiability Modulo Theories

摘要

Satisfiability Modulo Theories (SMT) studies methods for checking the satisfiability (or, dually, the validity) of first-order formulas with respect to some logical theory T of interest. What distinguishes SMT from general automated deduction is that the background theory T need not be finitely or even first-order axiomatizable, and that specialized inference methods are used for each theory. By being theory-specific and restricting their language to certain classes of formulas (such as, typically but not exclusively, ground formulas), these specialized methods can be implemented into solvers that are more efficient in practice than general-purpose theorem provers. While SMT techniques have been traditionally used to support deductive software verification, they are now finding applications in other areas of computer science such as, for instance, planning, model checking and automated test generation.Theory-specific solvers can be often described conveniently in terms of tableau calculi, especially if one wants to prove that a solver decides a certain fragment of a theory T. In practice, however, most modern SMT solvers are not tableau-based and follow one of two main approaches, both of which exploit the recent technological advances in SAT solving. The “eager” approach uses smart encodings to propositional logic to compile T-satisfiability problems into propositional satisfiability problems, which can then be solved by off-the-self SAT solvers. The “lazy” approach instead uses general run-time mechanisms to separate plain Boolean reasoning from theory reasoning proper, doing the latter with small specialized procedures, and delegating the former to a dedicated SAT engine based on the DPLL procedure.After a brief overview of SMT, this talk focuses on a general and extensible abstract framework, Abstract DPLL Modulo Theories, for modeling lazy STM solvers declaratively and studying some of their theoretical properties. The framework is used to present and discuss a few basic variants of the lazy approach, in the case of a single and of multiple background theories. The talk also presents an extension of the framework that drastically simplifies the implementation of theory-specific components, and could be of interest to implementors of ground tableaux calculi as well.