M. Bozzano; R. Bruttomesso; A. Cimatti; T. A. Junttila; R. Peter van; S. P. Schulz; R. Sebastiani,
MathSAT: Thigt Integration of SAT and Mathematical Decision Procedures,
Recent improvements in propositional satisfiability techniques (SAT) made it possible to tackle successfully some hard real-world problems (e.g. model-checking, circuit testing, propositional planning) by encoding into SAT.
However, a purely boolean representation is not expressive enough for many other real-world applications, including the verification of timed and hybrid systems, of proof obligations in software, and of circuit design at RTL level. These problems can be naturally modeled as satisfiability in Linear Arithmetic Logic (LAL), i.e., the boolean combination of propositional variables and linear constraints over numerical variables.
In this paper we present mathsat, a new, SAT-based decision procedure for LAL, based on the (known approach) of integrating a state-of-the-art SAT solver with a dedicated mathematical solver for LAL. We improve mathsat in two different directions.
First, the top level procedure is enhanced, and now features a tighter integration between the boolean search and the mathematical solver. In particular, we allow for theory-driven backjumping and learning, and theory-driven deduction; we use static learning in order to reduce the number of boolean models that are mathematically inconsistent; we exploit problem clustering in order to partition mathematical reasoning; and we define a stack-based interface that allows us to implement mathematical reasoning in an incremental and backtrackable way.
Second, the mathematical solver is based on layering, i.e. the consistency of (partial) assignments is checked in theories of increasing strength (equality and uninterpreted functions, linear arithmetic over the reals, linear arithmetic over the integers). For each of these layers, a dedicated (sub)solver is used. Cheaper solvers are called first, and detection of inconsistency makes calls of the subsequent solvers superfluous.
We provide a thorough experimental evaluation of our approach, by taking into account a large set of previously proposed benchmarks. We first investigate the relative benefits and drawbacks of each proposed technique by comparison with respect to a reference option setting. We then demonstrate the global effectiveness of our approach by a comparison with several state-of-the-art decision procedures. We show that the behavior of mathsat is often superior to its competitors, both on LAL, and in the subclass of Difference Logic,
M. Bozzano; R. Brutomesso; A. Cimatti; T. A. Junttila; S. Ranise; Rossen Peter van; R. Sebastiani,
Efficient Satisfiability Modulo Theories via Delayed Theory Combination,
The problem of deciding the satisfiability of a quantifier-free formula with respect to a background theory, also known as Satisfiability Modulo Theories (smt), is gaining increasing relevance in verification: representation capabilities beyond propositional logic allow for a natural modeling of real-world problems (e.g., pipeline and RTL circuits verification, proof obligations in software systems).
In this paper, we focus on the case where the background theory is the combination T1 U T2 of two simpler theories. Many smt procedures combine a boolean model enumeration with a decision procedure for T1 U T2, where conjunctions of literals can be decided by an integration schema such as Nelson-Oppen, via a structured exchange of interface formulae (e.g., equalities in the case of convex theories, disjunctions of equalities otherwise).
We propose a new approach for SMT(T1 U T2), called Delayed Theory Combination, which does not require a decision procedure for T1 U T2, but only individual decision procedures for T1 and T2, which are directly integrated to the boolean model enumerator.
This approach is much simpler and natural, allows each of the solvers to be implemented and optimized without taking into account the others, and it nicely encompasses the case of non-convex theories.
We show the effectiveness of the approach by a thorough experimental comparison,