Lazy Satisfiability Modulo Theories
Abstract
Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some decidable first-order theory
Typical
Unfortunately, neither the problem of building an efficient SMT solver, nor even that of acquiring a comprehensive background knowledge in lazy SMT, is of simple solution.
In this paper we present an extensive survey of SMT, with particular focus on the lazy approach. We survey, classify and analyze from a theory-independent perspective the most effective techniques and optimizations which are of interest for lazy SMT and which have been proposed in various communities; we discuss their relative benefits and drawbacks; we provide some guidelines about their choice and usage; we also analyze the features for SAT solvers and T -solvers which make them more suitable for an integration.
The ultimate goals of this paper are to become a source of a common background knowledge and terminology for students and researchers in different areas, to provide a reference guide for developers of SMT tools, and to stimulate the cross-fertilization of techniques and ideas among different communities.