Andreas Fröhlich, Gergely Kovasznai, Armin Biere,
"Efficiently Solving Bit-Vector Problems Using Model Checkers"
: Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13), University of Helsinki, Seite(n) 6-15, 2013
Original Titel:
Efficiently Solving Bit-Vector Problems Using Model Checkers
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13)
Original Kurzfassung:
Bit-precise reasoning is essential in many applications of
Satisfiability Modulo Theories (SMT). Most approaches for solving
quantifier-free fixed-size bit-vector logics (QF BV) rely on
bit-blasting. In previous work, we have shown that bit-blasting is not
polynomial in general [19], and later proposed QF BV<<1 , a class of
bit-vector problems that is PSpace-complete [15]. In this paper, we give
examples of how to create (polynomial) SMV specifications out of QF
BV<<1 formulas. We then use various model checkers to solve those
problems and give detailed experimental results. Our results show that
BDD-based model checkers outperform current SMT solvers by several
orders of magnitude on our benchmarks. Unrolling and using SAT-based
model checking turns out to be the same as bit-blasting and gives worse
results. In addition to this, our approach allows us to easily generate
new challenging benchmarks for SMT solvers as well as for model checkers.