A DPLL Algorithm for Solving DQBF

  • Andreas Fröhlich (Speaker)
  • Gergely Kovasznai (Speaker)
  • Armin Biere (Speaker)

Activity: Talk or presentation › Contributed talk › unknown

Description

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.
Period16 Jun 2012
Event titlePoS2012
Event typeConference
LocationItalyShow on map

Fields of science

  • 102 Computer Sciences
  • 101 Mathematics
  • 102011 Formal languages

JKU Focus areas

  • Computation in Informatics and Mathematics