Aina Niemetz, Mathias Preiner, Armin Biere,
"Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories"
: Proc. 28th Intl. Conf. on Computer Aided Verification (CAV'16), Serie Lecture Notes in Computer Science (LNCS), Vol. 9779, Springer, Seite(n) 199-217, 2016
Original Titel:
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 28th Intl. Conf. on Computer Aided Verification (CAV'16)
Original Kurzfassung:
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.
Forschungs-