Gergely Kovasznai, Andreas Fröhlich, Armin Biere,
"Complexity of Fixed-Size Bit-Vector Logics"
, in Theory of Computing Systems, Springer, Seite(n) 1-54, 9-2015, ISSN: 1432-4350
Original Titel:
Complexity of Fixed-Size Bit-Vector Logics
Sprache des Titels:
Englisch
Original Kurzfassung:
Bit-precise reasoning is important for many practical applications of Satisfiability Modulo
Theories (SMT). In recent years, efficient approaches for solving fixed-size bit-vector
formulas have been developed. From the theoretical point of view, only few results on the
complexity of fixed-size bit-vector logics have been published. Some of these results only
hold if unary encoding on the bit-width of bit-vectors is used.
In previous work [30], we have already shown that binary encoding adds more expressiveness
to bit-vector logics, e.g. it makes fixed-size bit-vector logic without uninterpreted
functions nor quantification NExpTime-complete.
In this paper, we revisit our complexity results for fixed-size bit-vector logics with
binary encoded bit-width and go into more detail when specifying the underlying logics
and presenting our proofs.
We also extend our previous work by analyzing commonly used bit-vector operations
showing how they can be represented by a minimal set of so-called base operations. We
further give a better insight in where the additional expressiveness of binary encoding comes
from by proposing some new complexity results for bit-vector logics with a restricted set
of base operations or certain conditions on the bit-width.
Sprache der Kurzfassung:
Englisch
Journal:
Theory of Computing Systems
Veröffentlicher:
Springer
Seitenreferenz:
1-54
Erscheinungsmonat:
9
Erscheinungsjahr:
2015
ISSN:
1432-4350
Anzahl der Seiten:
54
Reichweite:
international
Publikationstyp:
Aufsatz / Paper in sonstiger referierter Fachzeitschrift