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

Investor logo

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:

You are running an old browser version. We recommend updating your browser to its latest version.