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

DOI10.1016/J.IPL.2018.02.018MaRDI QIDQ1708270zbMATH OpenOpenAlexFDO

Authors Martin Jonáš, Jan Strejček

Publication date 5 April 2018

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1612.01263

zbMATH Keywords

computational complexitysatisfiability modulo theoriesfixed-size bit-vectors

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70)

Abstract: 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.

Recommendations

• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
• Complexity of fixed-size bit-vector logics
• On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
• Solving quantified bit-vector formulas using binary decision diagrams
• On the complexity of quantified integer programming

Cites work

• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• Alternation
• Axiomatizations for propositional and modal team logic
• Complexity of fixed-size bit-vector logics
• Constraint-Based Invariant Inference over Predicate Abstraction
• Efficiently solving quantified bit-vector formulas
• From program verification to program synthesis
• Model-checking hierarchical structures
• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
• On quantified propositional logics and the exponential time hierarchy
• Ranking function synthesis for bit-vector relations
• Theory of computation.
• Under-approximating loops in C programs for fast counterexample detection

Cited in

(4)

• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
• Canonical models and the complexity of modal team logic
• scientific article; zbMATH DE number 1346365 (Why is no real title available?)
• Complexity of fixed-size bit-vector logics

Describes a project that uses

Uses Software

• SymDIVINE

This page was built for publication: On the complexity of the quantified bit-vector arithmetic with binary encoding

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1708270)