Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

We described 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 approach relies on the combination of syntactic formula simplifications, tailored initial ordering of BDD variables, and using underapproximations and overapproximations, all of which help to reduce the size of the BDDs during the computation of the BDD corresponding to the input formula. The suggested approach has been implemented in the experimental open-source SMT solver called Q3B. 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, which solve quantified bit-vector formulas using the quantifier instantiation. Furthermore, we compared the implemented solver with the mentioned state-of-the art solvers on the quantified formulas produced by the symbolic model checker SymDIVINE. Again, the BDD based solver was able to decide more queries than Z3 and CVC4. Moreover, according to the preliminary results of the SMT competition 2016, Q3B is the best solver in the category of quantified bit-vectors, outperforming Z3, CVC4 and Boolector. Underapproximations used in the approach are performed by reducing the bit-width of all existentially quantified variables. Similarly, overapproximations are performed by reducing the bit-width of all existentially quantified variables. We describe several ways of reducing bit-width of a variable and we evaluate the effect of each of these on the performance of the solver. The publication with the detailed description of the approach, experimental results, and the evaluation of all three components used in the approach was accepted to SAT 2016.

Authors

• Martin Jonas

Keywords

No keywords are indexed for this paper.