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

TL;DR

This paper precisely characterizes the computational complexity of deciding satisfiability for quantified bit-vector formulas with binary encoding, establishing it as complete for the class AEXP(poly).

Contribution

It proves that the satisfiability problem for quantified bit-vector formulas with binary encoding is complete for the class AEXP(poly), refining previous complexity bounds.

Findings

The problem is in AEXP(poly) complexity class.

It is both in EXPSPACE and NEXPTIME-hard.

Provides a tight complexity classification for quantified bit-vector satisfiability.

Abstract

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 and constants. This problem is known to be in EXPSPACE and to be NEXPTIME-hard. We show that this problem is complete for the complexity class AEXP(poly) -- the class of problems decidable by an alternating Turing machine using exponential time, but only a polynomial number of alternations between existential and universal states.