Další formáty:
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 a Jan STREJČEK. On the complexity of the quantified bit-vector arithmetic with binary encoding. \textit{Information Processing Letters}. Elsevier, 2018, roč.~135, červenec 2018, s.~57-61. ISSN~0020-0190. Dostupné z: https://dx.doi.org/10.1016/j.ipl.2018.02.018.
|