More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding
Sprache des Vortragstitels:
8th Intl. Computer Science Symp. in Russia (CSR'13)
Sprache des Tagungstitel:
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.