Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

Kód výsledku v 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>
Výsledek na webu
<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>

Jazyk výsledku
angličtina
Název v původním jazyce
Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
Popis výsledku anglicky
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.

Projekt
<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění
2016
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku
Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference
ISBN
9783319409696
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
17
Strana od-do
267-283
Název nakladatele
Springer
Místo vydání
Berlin, Heidelberg
Místo konání akce
Bordeaux, France
Datum konání akce
1. 1. 2016
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—

Podobné výsledky(10)