Name
Title | ||
|---|---|---|
On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoded Bit-Widths. |
Abstract | ||
|---|---|---|
In this paper, we prove the precise computational complexity of deciding satisfiability of first-order quantified formulas over the theory of fixed-size bit-vectors. This problem is known to be solvable in exponential space 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 space and polynomial number of alternations between existential and universal states. |
Year | Venue | Field |
|---|---|---|
2016 | arXiv: Logic in Computer Science | Complexity class,PH,Structural complexity theory,Algorithm,Arithmetic,True quantified Boolean formula,Time complexity,Bit array,Mathematics,Computational complexity theory,Binary number |
DocType | Volume | Citations |
Journal | abs/1612.01263 | 0 |
PageRank | References | Authors |
0.34 | 0 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Martin Jonás | 1 | 4 | 2.10 |
| Jan Strejcek | 2 | 99 | 13.83 |