Satisfiability Modulo Theories (SMT) is essential for many applications in computer-aided verification. A recent SMT solving approach based on stochastic local search for the theory of quantifier-free fixed-size bit-vectors proved to be quite effective on hard satisfiable instances, particularly in the context of symbolic execution. However, it still relies on brute-force randomization and restarts to achieve completeness. In this paper we simplify, extend, and formalize the propagationbased variant of this approach. We introduce a notion of essential inputs to lift the well-known concept of controlling inputs from the bit-level to the word-level, which allows to prune search. Guided by a formal completeness proof for our propagation-based variant we obtain a clean, simple and more precise algorithm, which yields a substantial gain in performance, as shown in our experimental evaluation.
CITATION STYLE
Niemetz, A., Preiner, M., & Biere, A. (2016). Precise and complete propagation based local search for satisfiability modulo theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9779, pp. 199–217). Springer Verlag. https://doi.org/10.1007/978-3-319-41528-4_11
Mendeley helps you to discover research relevant for your work.