Gergely Kovasznai, Andreas Fröhlich, Armin Biere,
"On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width"
: Proc. 10th Intl. Workshop on Satisfiability Modulo Theories (SMT'12), Seite(n) 44-55, 2012
On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
Sprache des Titels:
Proc. 10th Intl. Workshop on Satisfiability Modulo Theories (SMT'12)
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. 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 functions
nor quantification NExpTime-complete. We also show that under certain restrictions
the increase of complexity when using binary encoding can be avoided.