Don't care in SMT - Buildin flexible yet efficient abstraction/refinement solver
Abstract
This paper describes a method for combining “off-the-shelf” SAT
and constraint solvers for building an efficient Satisfiability Modulo Theories
(SMT) solver for a wide range of theories. Our method follows the abstraction/
refinement approach to simplify the implementation of customSMT solvers.
The expected performance penalty by not using an interweaved combination of
SAT and theory solvers is reduced by generalising a Boolean solution of an
SMT problem first via assigning don't care to as many variables as possible. We
then use the generalised solution to determine a thereby smaller constraint set
to be handed over to the constraint solver for a background theory. We show
that for many benchmarks and real-world problems, this optimisation results in
considerably smaller and less complex constraint problems.
The presented approach is particularly useful for assembling a practically viable
SMT solver quickly, when neither a suitable SMT solver nor a corresponding incremental
theory solver is available. We have implemented our approach in the
ABSOLVER framework and applied the resulting solver successfully to an industrial
case-study: The verification problems arising in verifying an electronic
car steering control system impose non-linear arithmetic constraints, which do
not fall into the domain of any other available solver.