Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

JONÁŠ Martin STREJČEK Jan

Year of publication 2016
Type Article in Proceedings
Conference Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-40970-2_17
Field Informatics
Keywords SMT solving; quantified bit-vector formulas; BDD
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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.