Gergely Kovasznai, Andreas Fröhlich, Armin Biere,
"More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding"
: Proc. 8th Intl. Computer Science Symp. in Russia (CSR'13), Lecture Notes in Computer Science, Serie Lecture Notes in Computer Science, Springer, Seite(n) 378-390, 2013
Original Titel:
More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 8th Intl. Computer Science Symp. in Russia (CSR'13), Lecture Notes in Computer Science
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. Most
of these results only hold if unary encoding on the bit-width of
bit-vectors is used.
In previous work, we showed 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 look at the quantifier-free case again and propose two
new results. While it is enough to consider logics with bitwise
operations, equality, and shift by constant to derive
NEXPTIME-completeness, we show that the logic becomes PSPACE-complete
if, instead of shift by constant, only shift by 1 is permitted, and even
NP-complete if no shifts are allowed at all.
Forschungs-