Publication | Closed Access
Solving DQBF Through Quantifier Elimination
23
Citations
0
References
2015
Year
Circuit ComplexityStandard Qbf SolverEngineeringBoolean FunctionVerificationQuantifier EliminationComputer-aided VerificationComputational ComplexityFormal VerificationSatisfiabilityEquivalent QbfComputer EngineeringComputer ScienceEquational LogicQuantization (Signal Processing)Logic SynthesisAutomated ReasoningQuantificationFormal MethodsQuantifier Elimination Strategy
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.