Solving quantified bit-vector formulas using binary decision diagrams

DOI10.1007/978-3-319-40970-2_17zbMATH Open1475.68345OpenAlexW2474427045MaRDI QIDQ2818019FDOQ2818019

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

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

Mathematics Subject Classification ID

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

Cites Work

• Simplify: a theorem prover for program checking
• Graph-Based Algorithms for Boolean Function Manipulation
• Efficiently solving quantified bit-vector formulas
• A mathematical introduction to logic.
• 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: Generating all combinations and partitions. Fasc. 4: Generating all trees. History of combinatorial generation.
• Title not available (Why is that?)
• Efficient E-Matching for SMT Solvers
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Improving the variable ordering of OBDDs is NP-complete
• Deciding Bit-Vector Arithmetic with Abstraction
• Complexity of fixed-size bit-vector logics

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
• Deciding Bit-Vector Formulas with mcSAT
• Efficiently solving quantified bit-vector formulas
• Deciding Bit-Vector Arithmetic with Abstraction
• Title not available (Why is that?)
• Counterexample-Guided Model Synthesis
• Bitwuzla
• bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR
• MedleySolver: online SMT algorithm selection

Uses Software

• SMT-LIB
• z3
• SIMPLIFY
• CVC4

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)