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

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou 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.