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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability

  • Jakub Horák,
  • Martin Jonáš

摘要

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.