Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

DOI10.1007/978-3-319-40970-2_17zbMath1475.68345OpenAlexW2474427045MaRDI QIDQ2818019

Jan Strejček, Martin Jonáš

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)

Related Items (4)

Counterexample-Guided Model Synthesis ⋮ On solving quantified bit-vector constraints using invertibility conditions ⋮ MedleySolver: online SMT algorithm selection ⋮ DQBDD: an efficient BDD-based DQBF solver

Uses Software

• SMT-LIB
• z3
• SIMPLIFY
• CVC4

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Complexity of fixed-size bit-vector logics
• Efficiently solving quantified bit-vector formulas
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Simplify: a theorem prover for program checking
• Efficient E-Matching for SMT Solvers
• Graph-Based Algorithms for Boolean Function Manipulation
• Improving the variable ordering of OBDDs is NP-complete
• Deciding Bit-Vector Arithmetic with Abstraction

This page was built for publication: Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams