TY - GEN
T1 - BV2EPR: A Tool for Polynomially Translating Quantifier-free Bit-Vector Formulas into EPR
AU - Kovasznai, Gergely
AU - Fröhlich, Andreas
AU - Biere, Armin
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84879933264
U2 - 10.1007/978-3-642-38574-2_32
DO - 10.1007/978-3-642-38574-2_32
M3 - Conference proceedings
SN - 9783642385735
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 443
EP - 449
BT - CADE 2013 - 24th International Conference on Automated Deduction, Proceedings
PB - Springer
ER -