J 2018

On the complexity of the quantified bit-vector arithmetic with binary encoding

JONÁŠ, Martin a Jan STREJČEK

Základní údaje

Originální název

On the complexity of the quantified bit-vector arithmetic with binary encoding

Autoři

JONÁŠ, Martin (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

Information Processing Letters, Elsevier, 2018, 0020-0190

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Impakt faktor

Impact factor: 0.914

Kód RIV

RIV/00216224:14330/18:00100916

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000430518100011

Klíčová slova anglicky

computational complexity; satisfiability modulo theories; bit-vector theory

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 29. 4. 2019 15:54, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GBP202/12/G061, projekt VaV
Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky
MUNI/A/0854/2017, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty