J
2018
On the complexity of the quantified bit-vector arithmetic with binary encoding
JONÁŠ, Martin and Jan STREJČEK
Basic information
Original name
On the complexity of the quantified bit-vector arithmetic with binary encoding
Authors
JONÁŠ, Martin (203 Czech Republic, belonging to the institution) and
Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)
Edition
Information Processing Letters, Elsevier, 2018, 0020-0190
Other information
Type of outcome
Článek v odborném periodiku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Netherlands
Confidentiality degree
není předmětem státního či obchodního tajemství
Impact factor
Impact factor: 0.914
RIV identification code
RIV/00216224:14330/18:00100916
Organization unit
Faculty of Informatics
Keywords in English
computational complexity; satisfiability modulo theories; bit-vector theory
Tags
International impact, Reviewed
V originále
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.
Links
| GBP202/12/G061, research and development project | | Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI) | | Investor: Czech Science Foundation |
|
| MUNI/A/0854/2017, interní kód MU | | Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII. | | Investor: Masaryk University, Category A |
|
Displayed: 11/11/2024 11:55