Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR20-036 | 9th March 2020 15:27

Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths


Authors: Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl
Publication: 15th March 2020 11:16
Downloads: 668


We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new tautology-free DQBF dependency scheme that generalises the reflexive resolution path dependency scheme. We establish soundness of the tautology-free scheme, implying that it can be used in any DQBF proof system. We further explore the power of DQBF resolution systems parameterised by dependency schemes and show that our new scheme results in exponentially shorter proofs in comparison to the reflexive resolution path dependency scheme when used in the basic DQBF expansion proof system.

On QBFs, we demonstrate that our new scheme is exponentially stronger than the reflexive resolution path dependency scheme when used in Q Resolution, thus resulting in the strongest QBF dependency scheme known to date.

ISSN 1433-8092 | Imprint