More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding

Abstract

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 [1], 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-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-completeness, we show that the logic becomes-complete if, instead of shift by constant, only shift by 1 is permitted, and even-complete if no shifts are allowed at all. © 2013 Springer-Verlag Berlin Heidelberg.