On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoding
Logic in Computer Science
2018-05-03 v4
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.
Cite
@article{arxiv.1612.01263,
title = {On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoding},
author = {Martin Jonáš and Jan Strejček},
journal= {arXiv preprint arXiv:1612.01263},
year = {2018}
}