Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00088245" target="_blank" >RIV/00216224:14330/16:00088245 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-40970-2_17" target="_blank" >http://dx.doi.org/10.1007/978-3-319-40970-2_17</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-40970-2_17" target="_blank" >10.1007/978-3-319-40970-2_17</a>
Alternative languages
Result language
angličtina
Original language name
Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference
ISBN
9783319409696
ISSN
0302-9743
e-ISSN
—
Number of pages
17
Pages from-to
267-283
Publisher name
Springer
Place of publication
Berlin, Heidelberg
Event location
Bordeaux, France
Event date
Jan 1, 2016
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—