Aina Niemetz, Mathias Preiner, Armin Biere, Andreas Fröhlich,
"Improving Local Search For Bit-Vector Logics in SMT with Path Propagation"
: Proc. 4th Intl. Work. on Design and Implementation of Formal Tools and Systems (DIFTS'15), FMCAD Inc. 2015, 2015
Original Titel:
Improving Local Search For Bit-Vector Logics in SMT with Path Propagation
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 4th Intl. Work. on Design and Implementation of Formal Tools and Systems (DIFTS'15)
Original Kurzfassung:
Bit-blasting is the main approach for solving
word-level constraints in SAT Modulo Theories (SMT) for
bit-vector logics. However, in practice it often reaches its
limits, even if combined with sophisticated rewriting and
simplification techniques. In this paper, we extended a recently
proposed alternative based on stochastic local search
(SLS) and improve neighbor selection based on down
propagation of assignments. We further reimplemented
the previous SLS approach in our SMT solver Boolector
and confirm its effectiveness. We then added our novel
propagation-based extension and provide an extensive experimental
evaluation, which suggests that combining these
techniques with Boolector?s bit-blasting engine enables
Boolector to solve substantially more instances.
Forschungs-