Don't care in SMT: Building flexible yet efficient abstraction/refinement solvers
Date
2010
Authors
Bauer, Andreas
Leucker, Martin
Schallhart, Christian
Tautschnig, Michael
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
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 custom SMT 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.
Description
Keywords
Keywords: Background theory; Constraint problems; Constraint set; Constraint solver; Constraint solvers; Non-linear; Optimisations; Performance penalties; Real-world problem; Satisfiability modulo Theories; Steering control system; Theory solvers; Verification prob Constraint solver; SMT; Verification
Citation
Collections
Source
International Journal on Software Tools for Technology Transfer
Type
Journal article
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31