Arrow Research search

Author name cluster

Aile Ge-Ernst

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
1 author row

Possible papers

2

TCS Journal 2022 Journal Article

Solving dependency quantified Boolean formulas using quantifier localization

  • Aile Ge-Ernst
  • Christoph Scholl
  • Juraj Síč
  • Ralf Wimmer

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 which can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, research focused on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula), while 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 all instances from the QBFEVAL'18–'20 competitions, clearly show that quantifier localization pays off in this context.

Details DOI

AAAI Conference 2019 Conference Paper

A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving

  • Christoph Scholl
  • Jie-Hong Roland Jiang
  • Ralf Wimmer
  • Aile Ge-Ernst

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. This enables a succinct encoding of decision problems in the NEXPTIME complexity class. As solving general DQBFs is NEXPTIME complete, in contrast to the PSPACE completeness of QBF solving, characterizing DQBF subclasses of lower computational complexity allows their effective solving and is of practical importance. 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 ΣP 3 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.

PDF Details
v2026.09.13