Complexity of fixed-size bit-vector logics

DOI10.1007/s00224-015-9653-1zbMath1357.68086OpenAlexW2211407346MaRDI QIDQ504997

Andreas Fröhlich, Gergely Kovásznai, Armin Biere

Publication date: 18 January 2017

Published in: Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00224-015-9653-1

zbMATH Keywords

complexitySATSMTsatisfiability modulo theoriesPSPACEbit-vectorsNPbinary encodingbit-vector logicslogarithmic encodingNEXPTIMEunary encoding

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

A bit-vector differential model for the modular addition by a constant and its applications to differential and impossible-differential cryptanalysis ⋮ A bit-vector differential model for the modular addition by a constant ⋮ On the complexity of the quantified bit-vector arithmetic with binary encoding ⋮ Counterexample-Guided Model Synthesis ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ Wombit: a portfolio bit-vector solver using word-level propagation

Uses Software

• Boolector
• SMT-LIB
• NuSMV
• Yices
• z3
• MONA
• bv2epr
• MathSAT
• iProver
• NASA PVS
• STP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Complexity results for classes of quantificational formulas
• Efficiently solving quantified bit-vector formulas
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Relationships between nondeterministic and deterministic tape complexities
• Henkin Quantifiers and Boolean Formulae
• Synthesis for Unbounded Bit-Vector Arithmetic
• SAT-Based Model Checking without Unrolling
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Ranking Function Synthesis for Bit-Vector Relations
• The complexity of propositional linear temporal logics
• `` Strong NP-Completeness Results
• bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR
• More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding
• A Decision Procedure for Bit-Vectors and Arrays
• Deciding Bit-Vector Arithmetic with Abstraction
• Verification, Model Checking, and Abstract Interpretation
• Lower bounds for multiplayer noncooperative games of incomplete information