MATHSAT: Tight Integration of SAT and Mathematical Decision Procedures
M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila,
P. van Rossum, S. Schulz and R. Sebastiani
Recent improvements in propositional satisfiability techniques (SAT)
made it possi- ble 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 MAT H S AT, 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 mathe- matical solver for
LAL. We improve MAT H S AT 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 parti- tion 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 MAT H S AT is often superior to its competitors,
both on LAL, and in the subclass of Difference Logic.