Aina Niemetz, Mathias Preiner, Armin Biere,
"Propagation Based Local Search for Bit-Precise Reasoning"
: Journal of Formal Methods in System Design, Serie Formal Methods in System Design, Vol. 51, Nummer 3, Springer, Seite(n) 608-636, 12-2017
Propagation Based Local Search for Bit-Precise Reasoning
Sprache des Titels:
Journal of Formal Methods in System Design
Many applications of computer-aided veri?cation require bit-precise reasoning as provided by Satis?ability Modulo Theories (SMT) solvers for the theory of quanti?er-free ?xed-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 e?cient in practice, but may not scale if the input size can not be reduced su?ciently during preprocessing. A recent score-based local search approach lifts stochastic local search (SLS) from the bit-level (SAT) to the word-level (SMT) without bit-blasting and proved to be quite e?ective on hard satis?able 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 simpli?ed, 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 e?ects.