Solving quantified bit-vector formulas using binary decision diagrams

DOI10.1007/978-3-319-40970-2_17MaRDI QIDQ2818019zbMATH OpenOpenAlexFDO

Authors Martin Jonáš, Jan Strejček

Publication date 5 September 2016

Published in Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-40970-2_17

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Abstraction of bit-vector operations for BDD-based SMT solvers
• Efficiently solving quantified bit-vector formulas
• Solving quantified bit-vectors using invertibility conditions
• On solving quantified bit-vector constraints using invertibility conditions
• Deciding Bit-Vector Arithmetic with Abstraction

Cites work

• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• A mathematical introduction to logic.
• Complexity of fixed-size bit-vector logics
• Deciding Bit-Vector Arithmetic with Abstraction
• Efficient E-Matching for SMT Solvers
• Efficiently solving quantified bit-vector formulas
• Graph-Based Algorithms for Boolean Function Manipulation
• Improving the variable ordering of OBDDs is NP-complete
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Simplify: a theorem prover for program checking
• The art of computer programming. Vol. 4, Fasc. 0--4. Fasc. 0: Introduction to combinatorial algorithms and Boolean functions. Fasc. 1: Bitwise tricks \& techniques, binary decision diagrams. Fasc. 2: Generating all tuples and permutations. Fasc. 3: Genera

Cited in

(15)

• On the complexity of the quantified bit-vector arithmetic with binary encoding
• DQBDD: an efficient BDD-based DQBF solver
• Abstraction of bit-vector operations for BDD-based SMT solvers
• On solving quantified bit-vector constraints using invertibility conditions
• Truncating abstraction of bit-vector operations for BDD-based SMT solvers
• On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
• Solving quantified bit-vectors using invertibility conditions
• Efficiently solving quantified bit-vector formulas
• Deciding Bit-Vector Formulas with mcSAT
• Deciding Bit-Vector Arithmetic with Abstraction
• scientific article; zbMATH DE number 846270 (Why is no real title available?)
• Counterexample-Guided Model Synthesis
• bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR
• Bitwuzla
• MedleySolver: online SMT algorithm selection

Describes a project that uses

Uses Software

• CVC4
• SIMPLIFY
• z3
• SMT-LIB

This page was built for publication: Solving quantified bit-vector formulas using binary decision diagrams

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