More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding

Description

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.

Period	28 Jun 2013
Event title	8th Intl. Computer Science Symp. in Russia (CSR'13)
Event type	Conference
Location	Russian FederationShow on map