Propagation based local search for bit-precise reasoning
Aina Niemetz, Mathias Preiner, Armin Biere · Formal Methods in System Design · 2017
Many applications of computer-aided verification require bit-precise reasoning as provided by satisfiability modulo theories (SMT) solvers for the theory of quantifier-free fixed-size bit-vectors. The current state-of-the-art in solving bit-vector formulas in SMT relies on bit-blasting, where a given formula is eagerly translated into propositional logic (SAT) and handed to an underlying SAT solver. Bit-blasting is efficient in practice, but may not scale if the input size can not be reduced sufficiently during preprocessing. A recent score-based local search approach lifts stochastic local search from the bit-level (SAT) to the word-level (SMT) without bit-blasting and 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. Guided by a completeness proof, we simplified, extended and formalized our propagation-based variant of this approach. We obtained a clean, simple and more precise algorithm that does not rely on score-based local search techniques and does not require brute-force randomization or restarts to achieve completeness. It further yields substantial gain in performance. In this article, we present and discuss our complete propagation based local search approach for bit-vector logics in SMT in detail. We further provide an extended and extensive experimental evaluation including an analysis of randomization effects.