Stochastic Local Search for Satisfiability Modulo Theories


  • Andreas Fröhlich Johannes Kepler University
  • Armin Biere Johannes Kepler University
  • Christoph Wintersteiger Microsoft
  • Youssef Hamadi Microsoft



Satisfiability Modulo Theories, Stochastic Local Search, Bit-Vectors


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.




How to Cite

Fröhlich, A., Biere, A., Wintersteiger, C., & Hamadi, Y. (2015). Stochastic Local Search for Satisfiability Modulo Theories. Proceedings of the AAAI Conference on Artificial Intelligence, 29(1).



AAAI Technical Track: Heuristic Search and Optimization