Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1357165,
author = {Jonáš, Martin and Strejček, Jan},
address = {Berlin, Heidelberg},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference},
doi = {http://dx.doi.org/10.1007/978-3-319-40970-2_17},
editor = {Nadia Creignou and Daniel Le Berre},
keywords = {SMT solving; quantified bit-vector formulas; BDD},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Berlin, Heidelberg},
isbn = {978-3-319-40969-6},
pages = {267-283},
publisher = {Springer},
title = {Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams},
year = {2016}
}
TY - JOUR
ID - 1357165
AU - Jonáš, Martin - Strejček, Jan
PY - 2016
TI - Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
PB - Springer
CY - Berlin, Heidelberg
SN - 9783319409696
KW - SMT solving
KW - quantified bit-vector formulas
KW - BDD
N2 - We describe a new approach to deciding satisfiability of quantified bit-vector formulas using binary decision diagrams and approximations. The approach is motivated by the observation that the binary decision diagram for a quantified formula is typically significantly smaller than the diagram for the subformula within the quantifier scope. The suggested approach has been implemented and the experimental results show that it decides more benchmarks from the SMT-LIB repository than state-of-the-art SMT solvers for this theory, namely Z3 and CVC4.
ER -
JONÁŠ, Martin and Jan STREJČEK. Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. In Nadia Creignou and Daniel Le Berre. \textit{Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference}. Berlin, Heidelberg: Springer, 2016, p.~267-283. ISBN~978-3-319-40969-6. Available from: https://dx.doi.org/10.1007/978-3-319-40970-2\_{}17.
|
