Gergely Kovasznai, Andreas Fröhlich, Armin Biere,
"BV2EPR: A Tool for Polynomially Translating Quantifier-free Bit-Vector Formulas into EPR"
: Proc. 24th Intl. Conf. on Automated Deduction (CADE'13), Lecture Notes in Computer Science, Serie LNCS, Springer, Seite(n) 443-449, 2013
Original Titel:
BV2EPR: A Tool for Polynomially Translating Quantifier-free Bit-Vector Formulas into EPR
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 24th Intl. Conf. on Automated Deduction (CADE'13), Lecture Notes in Computer Science
Original Kurzfassung:
Bit-precise reasoning is essential in many applications of
Satisfiability Modulo Theories (SMT). In recent years, efficient
approaches for solving fixed-size bit-vector formulas have been
developed. Most of these approaches rely on bit-blasting. In [1], we
argued that bit-blasting is not polynomial in general, and then showed
that solving quantifier-free bit-vector formulas (QF_BV) is
NEXPTIME-complete. In this paper, we present a tool based on a new
polynomial translation from QF_BV to Effectively Propositional Logic
(EPR). This allows us to solve QF_BV-problems using EPR-solvers and
avoids the exponential growth that comes with bit-blasting.
Additionally, our tool allows us to easily generate new challenging
benchmarks for EPR solvers.
Forschungs-