From DQBF to QBF by Dependency Elimination
Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker · MPG.PuRe (Max Planck Society) · 2018
Dependency quantified Boolean formulas (DQBFs) are a generalization of QBFs, which allows to have existential variables that depend on arbitrary subsets of the universal variables. We present an effective way to solve such DQBFs by eliminating individual dependencies such that an equisatisfiable QBF is obtained, which can be solved by an arbitrary QBF solver. We also present how to use dependency schemes in order to obtain smaller equisatisfiable QBFs, which can typically be solved more efficiently.