On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoding

Martin Jonáš, Jan Strejček

We study the precise computational complexity of deciding satisfiability of first-order quantified formulas over the theory of fixed-size bit-vectors with binary-encoded bit-widths…