2021

 nach oben zur Jahresübersicht

• Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer
  Solving Dependency Quantified Boolean Formulas Using Quantifier Localization
  CoRR, Band: 1905.04755, 2021

2019

 nach oben zur Jahresübersicht

• Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, Aile Ge-Ernst
  A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving
  2019 33th AAAI Conference on Artificial Intelligence (AAAI-19)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Recently a DQBF proof calculus based on a notion of fork extension, in addition to resolution and universal reduction, was proposed by Rabe in 2017. We show that this calculus is in fact incomplete for general DQBFs, but complete for a subclass of DQBFs, where any two existential variables have either identical or disjoint dependency sets over the universal variables. We further characterize this DQBF subclass to be SigmaP3 complete in the polynomial time hierarchy. Essentially using fork extension, a DQBF in this subclass can be converted to an equisatisfiable 3QBF with only a linear increase in formula size. We exploit this conversion for effective solving of this DQBF subclass and point out its potential as a general strategy for DQBF quantifier localization. Experimental results show that the method outperforms state-of-the-art DQBF solvers on a number of benchmarks, including the 2018 DQBF evaluation benchmarks.
• Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer
  Localizing Quantifiers for DQBF
  2019 Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD), IEEE Computer Society Press
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Dependency quantified Boolean formulas (DQBFs)are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various applications that can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, most works focus on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula), and non-prenex DQBFs have almost not been studied in the literature. In this paper we provide a formal definition for syntax and semantics of non-closed non-prenex DQBFs and prove useful properties enabling quantifier localization. Moreover, we make use of our theory by integrating quantifier localization into a state-of-the art DQBF solver. Experiments with prenex DQBF benchmarks, including those from the QBFEVAL’18 competition, clearly show that quantifier localization pays off in this context.
• Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer
  Quantifier Localization for DQBF
  2019 Int'l Workshop on Logic and Synthesis
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  that quantifier localization pays off in this context.