From DQBF to QBF by Dependency Elimination

Abstract

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.