A DPLL Algorithm for Solving DQBF

Beschreibung

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 ap- plied in similar algorithms for SAT/QBF can be lifted to this richer logic. This enables to reuse efficient SAT and QBF solving techniques.

Zeitraum	16 Juni 2012
Ereignistitel	PoS2012
Veranstaltungstyp	Konferenz
Ort	ItalienAuf Karte anzeigen