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. In this paper we show that some of these results only hold if unary encoding on the bit-width of bit-vectors is used. We then consider fixed-size bit-vector logics with binary encoded bit-width and establish new complexity results. Our proofs show that binary encoding adds more expressiveness to bit-vector logics, e.g. it makes fixed-size bit-vector logic even without uninterpreted func- tions nor quantification NExpTime-complete. We also show that under certain restrictions the increase of complexity when using binary encoding can be avoided.

Period	30 Jun 2012
Event title	SMT 2012
Event type	Conference
Location	United KingdomShow on map