Other formats:
BibTeX
LaTeX
RIS
@article{1415323,
author = {Jonáš, Martin and Strejček, Jan},
article_number = {červenec 2018},
doi = {http://dx.doi.org/10.1016/j.ipl.2018.02.018},
keywords = {computational complexity; satisfiability modulo theories; bit-vector theory},
language = {eng},
issn = {0020-0190},
journal = {Information Processing Letters},
title = {On the complexity of the quantified bit-vector arithmetic with binary encoding},
url = {https://www.sciencedirect.com/science/article/pii/S0020019018300474},
volume = {135},
year = {2018}
}
TY - JOUR
ID - 1415323
AU - Jonáš, Martin - Strejček, Jan
PY - 2018
TI - On the complexity of the quantified bit-vector arithmetic with binary encoding
JF - Information Processing Letters
VL - 135
IS - červenec 2018
SP - 57-61
EP - 57-61
PB - Elsevier
SN - 00200190
KW - computational complexity
KW - satisfiability modulo theories
KW - bit-vector theory
UR - https://www.sciencedirect.com/science/article/pii/S0020019018300474
L2 - https://www.sciencedirect.com/science/article/pii/S0020019018300474
N2 - 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.
ER -
JONÁŠ, Martin and Jan STREJČEK. On the complexity of the quantified bit-vector arithmetic with binary encoding. \textit{Information Processing Letters}. Elsevier, 2018, vol.~135, červenec 2018, p.~57-61. ISSN~0020-0190. Available from: https://dx.doi.org/10.1016/j.ipl.2018.02.018.
|
