A DPLL Algorithm for Solving DQBF
Andreas Fröhlich, Gergely Kovásznai, Armin Biere · 2012
Abstract. Dependency Quantified Boolean Formulas (DQBF) comprise the set of propositional formulas which can be formulated by adding Henkin quantifiers to Boolean logic. We are not aware of any published attempt in solving this class of formulas in practice. However with DQBF being NEXPTIME-complete, efficient ways of solving it would have many practical applications. In this paper we describe a DPLL-style approach (DQDPLL) for solving DQBF. We show how methods successfully applied in similar algorithms for SAT/QBF can be lifted to this richer logic. This enables to reuse efficient SAT and QBF solving techniques. 1