Proc. Intl. Workshop on Pragmatics of SAT (POS'14),
Original Kurzfassung:
Dependency Quantified Boolean Formulas (DQBF) are obtained by adding Henkin
quantifiers to Boolean formulas and have seen growing interest in the last years. Since deciding
DQBF is NExpTime-complete, efficient ways of solving it would have many practical
applications. Still, there is only few work on solving this kind of formulas in practice. In
this paper, we present an instantiation-based technique to solve DQBF efficiently. Apart
from providing a theoretical foundation, we also propose a concrete implementation of our
algorithm. Finally, we give a detailed experimental analysis evaluating our prototype iDQ
on several DQBF as well as QBF Benchmarks.