13 - Tractability and Modern Satisfiability Modulo Theories Solvers
from Part 5 - Heuristics
Published online by Cambridge University Press: 05 February 2014
Summary
Satisfiability Modulo Theories (SMT) extends Propositional Satisfiability with logical theories that allow us to express relations over various types of variables, such as arithmetic constraints, or equalities over uninterpreted functions. SMT solvers are widely used in areas such as software verification, where they are able to solve surprisingly efficiently some problems that appear hard, when not undecidable. This chapter presents a general introduction to SMT solving. It then focuses on one important theory, equality, and gives both a detailed understanding of how it is solved, and a theoretical justiication of why the procedure is practically effective.
Introduction
Our starting point is research and experiences in the context of the state-of-the art SMT solver Z3 [13], developed by the authors at Microsoft Research. We first cover a selection of the main challenges and techniques for making SMT solving practical, integrating algorithms for tractable subproblems, and pragmatics and heuristics used in practice. We then take a proof-theoretical perspective on the power and scope of the engines used by SMT solvers. Most modern SMT solvers are built around a tight integration with efficient SAT solving. The framework is commonly referred to as DPLL(T), where T refers to a theory or a combination of theories. The theoretical result we present compares DPLL(T) with unrestricted resolution. A straightforward adaption of DPLL(T) provides a weaker proof system than unrestricted resolution, and we investigate an extension we call Conflict Directed Theory Resolution as a candidate method for bridging this gap. Our results apply to the case where T is the theory of equality.
- Type
- Chapter
- Information
- TractabilityPractical Approaches to Hard Problems, pp. 350 - 377Publisher: Cambridge University PressPrint publication year: 2014
- 2
- Cited by