max planck institut
informatik
informatik
Procedures to decide formulas in combinations of quantifier-free first-order theories, recently dubbed Satisfiability Modulo Theories or SMT, have been used to solve problems in a wide range of applications including hardware and software verification. Examples of SMT formulas include those arising in RTL datapath verification, symbolic timing verification, and buffer over-run vulnerability detection. In the past several years, considerable progress was made in solving these types of problems by leveraging the reasoning and learning power of Boolean SAT solving techniques and combining them with methods for deciding the satisfiability of the other theories.
In this work, we present a new SAT-based progressive approach for building scalable and efficient decision procedures for SMT problems. Specifically, for verification applications, an SMT instance is naturally decomposed into subproblems in the theories of a) Propositional Logic, b) Equality with Uninterpreted Functions, c) Unit-Two-Variable-Per-Inequality (UTVPI) Logic, and d) Linear Integer Arithmetic (LIA). Our algorithmic framework, which we refer to as Mixed Logical Integer Linear Programming (MLILP), is based on introducing new propsotional "indicator" variables to represent the theory atoms/constraints, and yields a purely propositional asbtraction of the problem. This abstraction serves as the "glue" that ties together the different theories and forms the basis for reasoning and learning within and across theories. In particular, assigning true to an indicator variable activates its corresponding theory constraint and invokes the appropriate theory solver to propagate the effect of adding this constraint. The framework allows for implications to flow through the theory solvers to activate other theory constraints based on the current assignments, or to flag violations. Conflict-based learning is extended to enable the creation of learned propositional clauses, as well as more expressive theory constraints that significantly increase the prunign power of the scheme. The framework is flexible enough to permit a tight or a loose integration of theory solvers based on their computational overhead. For example, the UTVPI theory solver, which is based on transitive closure, is tightly integrated whereas the more general LIA solver is loosely integrated. We will describe how different integration strategies impact the scalability and performance of the overall solver on a variety of hardware and software verification benchmarks.