Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF

Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate Schmidt, Martin Suda

Research output: Contribution to journalArticlepeer-review

Abstract

Dependency quantified Boolean formulas (DQBF) and QBF dependency schemes have been treated separately in the literature, even though both treatments extend QBF by replacing the linear order of the quantifier prefix with a partial order. We propose to merge the two, by reinterpreting a dependency scheme as a mapping from QBF into DQBF. Our approach offers a fresh insight on the nature of soundness in proof systems for QBF with dependency schemes, in which a natural property called ‘full exhibition’ is central. We apply our approach to QBF proof systems from two distinct paradigms, termed ‘universal reduction’ and ‘universal expansion’. We show that full exhibition is sufficient (but not necessary) for soundness in universal reduction systems for QBF with dependency schemes, whereas for expansion systems the same property characterises soundness exactly. We prove our results by investigating DQBF proof systems, and then employing our reinterpretation of dependency schemes. Finally, we show that the reflexive resolution path dependency scheme is fully exhibited, thereby proving a conjecture of Slivovsky.
Original languageEnglish
Pages (from-to)597–623
JournalJournal of Automated Reasoning
Volume63
Issue number0
Early online date24 Sep 2018
DOIs
Publication statusPublished - 2018

Keywords

  • DQBF
  • Dependency schemes
  • F.2.2 Nonnumerical algorithms and problems
  • Quantified Boolean formulas

Fingerprint

Dive into the research topics of 'Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF'. Together they form a unique fingerprint.

Cite this