|
doi: 10.7873/DATE.2015.0098
Solving DQBF Through Quantifier Elimination
Karina Gitinaa, Ralf Wimmerb, Sven Reimerc, Matthias Sauerd, Christoph Scholle and Bernd Beckerf
Institute of Computer Science, Albert-Ludwigs-Universität Freiburg Georges-Köhler-Allee,
D-79110 Freiburg, Germany.
agitina@informatik.uni-freiburg.de
bwimmer@informatik.uni-freiburg.de
creimer@informatik.uni-freiburg.de
dsauerm@informatik.uni-freiburg.de
escholl@informatik.uni-freiburg.de
fbeckerg@informatik.uni-freibur.de
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.
Full Text (PDF)
|