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

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	JONÁŠ Martin STREJČEK Jan
Year of publication	2018
Type	Article in Periodical
Magazine / Source	Information Processing Letters
MU Faculty or unit	Faculty of Informatics
Citation
Web	https://www.sciencedirect.com/science/article/pii/S0020019018300474
Doi	http://dx.doi.org/10.1016/j.ipl.2018.02.018
Keywords	computational complexity; satisfiability modulo theories; bit-vector theory
Description	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.
Related projects:	Centrum excelence - Institut teoretické informatiky Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.