Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-40970-2_17 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Discrete mathematics,Computer science,Satisfiability,Binary decision diagram,Algorithm,Diagram,Bit array | Conference | 9710 |
ISSN | Citations | PageRank |
0302-9743 | 3 | 0.45 |
References | Authors | |
13 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Martin Jonás | 1 | 3 | 2.48 |
| Jan Strejcek | 2 | 99 | 13.83 |