Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6874184 | Information Processing Letters | 2018 | 5 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
M. JonáÅ¡, J. StrejÄek,