Proc. Intl. Workshop on Pragmatics of SAT (POS'12)
Original Kurzfassung:
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.