BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability
摘要
We propose a technique that combines a bdd-based solver for quantified bit-vector formulas with an arbitrary other solver. The main idea is to employ the bdd-based solver on subformulas of the problem and then add the obtained information back to the original formula. The technique relies on a preexisting algorithm for computing approximate bdds for the given quantified bit-vector formula and on a novel algorithm that translates the resulting bdd back to a bit-vector formula while preserving some word-level information. The experimental evaluation shows that the proposed technique can improve performance of existing state-of-the-art smt solvers and can decide satisfiability of some formulas that were beyond reach of all the compared solvers.