On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width

Description

Bit-precise reasoning is important for many practical applications of Satisfiability Mod- ulo 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 [26] we’ve already shown that binary encoding adds more expressive- ness to bit-vector logics, e.g. it makes fixed-size bit-vector logic even 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 specifiying the underlying logics and presenting our proofs. We also extend our previous work by analyzing commonly used bit-vector operators 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.

Period	27 Sept 2012
Event title	PUMA Workshop
Event type	Conference
Location	AustriaShow on map