Stochastic Local Search for Satisfiability Modulo Theories
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 29th AAAI Conf. (AAAI15)
Original Kurzfassung:
Satisfiability Modulo Theories (SMT) is essential for many
practical applications, e.g., in hard- and software verification,
and increasingly also in other scientific areas like computational
biology. A large number of applications in these areas
benefit from bit-precise reasoning over finite-domain variables.
Current approaches in this area translate a formula over
bit-vectors to an equisatisfiable propositional formula, which
is then given to a SAT solver. In this paper, we present a novel
stochastic local search (SLS) algorithm to solve SMT problems,
especially those in the theory of bit-vectors, directly
on the theory level. We explain how several successful techniques
used in modern SLS solvers for SAT can be lifted
to the SMT level. Experimental results show that our approach
can compete with state-of-the-art bit-vector solvers on
many practical instances and, sometimes, outperform existing
solvers. This offers interesting possibilities in combining our
approach with existing techniques, and, moreover, new insights
into the importance of exploiting problem structure in
SLS solvers for SAT. Our approach is modular and, therefore,
extensible to support other theories, potentially allowing SLS
to become part of the more general SMT framework.
Forschungs-