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

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

JONÁŠ Martin STREJČEK Jan

Rok publikování 2018
Druh Článek v odborném periodiku
Časopis / Zdroj Information Processing Letters
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://www.sciencedirect.com/science/article/pii/S0020019018300474
Doi http://dx.doi.org/10.1016/j.ipl.2018.02.018
Klíčová slova computational complexity; satisfiability modulo theories; bit-vector theory
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.