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.

2016

 nach oben zur Jahresübersicht

• Valeriy Balabanov, Jie-Hong Roland Jiang, Christoph Scholl, Alan Mishchenko, Robert K. Brayton
  2QBF: Challenges and Solutions
  2016 International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer-Verlag, Nummer: 9710, Seiten: 453 - 469
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  2QBF is a special form \forall x \exists y. \Phi of the quantified Boolean formula (QBF) restricted to only two quantification layers, where \Phi is a quantifier-free formula. Despite its restricted form, it provides a framework for a wide range of applications, such as artificial intelligence, graph theory, synthesis, etc. In this work, we overview two main 2QBF challenges in terms of solving and certification. We contribute several improvements to existing solving approaches and study how the corresponding approaches affect certification. We further conduct an extensive experimental comparison on both competition and application benchmarks to demonstrate strengths of the proposed methodology.