TY - GEN
T1 - Quantifier-Free Bit-Vector Formulas with Binary Encoding: Benchmark Description.
AU - Kovasznai, Gergely
AU - Fröhlich, Andreas
AU - Biere, Armin
PY - 2013
Y1 - 2013
N2 - it-precise reasoning over fixed-size bit-vector logics
(QF_BV) is important for many practical applications of Satisfability
Modulo Theories (SMT), particularly for hardware and software
verifcation. In [1], we argued that a logarithmic (w.l.o.g. binary)
encoding, as used e.g. in the SMT-LIB format [2], leads to
NExpTime-completeness of the underlying decision problem. Bit-blasting,
as used in most current SMT solvers, therefore produces exponentially
larger CNF formulas on certain QF_BV formulas. We provide generation
scripts for several sets of QF_BV benchmarks in SMT-LIB format where
this is the case and use bit-blasting to generate SAT benchmarks out of
the original SMT2 specifications. All scripts and generated benchmarks
are available at http://fmv.jku.at/smtbench.
AB - it-precise reasoning over fixed-size bit-vector logics
(QF_BV) is important for many practical applications of Satisfability
Modulo Theories (SMT), particularly for hardware and software
verifcation. In [1], we argued that a logarithmic (w.l.o.g. binary)
encoding, as used e.g. in the SMT-LIB format [2], leads to
NExpTime-completeness of the underlying decision problem. Bit-blasting,
as used in most current SMT solvers, therefore produces exponentially
larger CNF formulas on certain QF_BV formulas. We provide generation
scripts for several sets of QF_BV benchmarks in SMT-LIB format where
this is the case and use bit-blasting to generate SAT benchmarks out of
the original SMT2 specifications. All scripts and generated benchmarks
are available at http://fmv.jku.at/smtbench.
M3 - Conference proceedings
VL - B-2013-1
T3 - Department of Computer Science Series of Publications B
SP - 107
EP - 108
BT - Proceedings of SAT Competition 2013
A2 - A. Balint, A. Belov, M. Heule, M. Järvisalo, null
PB - University of Helsinki,
ER -