Gergely Kovasznai, Andreas Fröhlich, Armin Biere,
"Quantifier-Free Bit-Vector Formulas with Binary Encoding: Benchmark Description."
, in A. Balint, A. Belov, M. Heule, M. Järvisalo: Proceedings of SAT Competition 2013, Serie Department of Computer Science Series of Publications B, Vol. B-2013-1, University of Helsinki,, Seite(n) 107-108, 2013
Original Titel:
Quantifier-Free Bit-Vector Formulas with Binary Encoding: Benchmark Description.
Sprache des Titels:
Englisch
Original Buchtitel:
Proceedings of SAT Competition 2013
Original Kurzfassung:
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.
Sprache der Kurzfassung:
Englisch
Veröffentlicher:
University of Helsinki,
Serie:
Department of Computer Science Series of Publications B