Improving Local Search for Bit-Vector Logics with Path Propagation
Sprache des Vortragstitels:
Englisch
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