Solving DQBF through quantifier elimination

Abstract

We show how to solve dependency quantified Boolean formulas (DQBF) using a quantifier elimination strategy which yields an equivalent QBF that can be decided using any standard QBF solver. The elimination is accompanied by a number of optimizations which help reduce memory consumption and computation time. We apply our solver HQS to problems from the domain of verification of incomplete combinational circuits to demonstrate the effectiveness of the proposed algorithm. The results show enormous improvements both in the number of solved instances and in the computation times compared to existing work on validating DQBF.