Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

All reports by Author Joshua Blinkhorn:

TR21-135 | 6th September 2021
Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl

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

We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new infinite collection of implication-free DQBF dependency schemes that generalise the reflexive resolution path dependency scheme. We establish soundness of all these schemes, implying that they can be ... more >>>

TR20-188 | 12th December 2020
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, Gaurav Sood

Hard QBFs for Merge Resolution

Revisions: 1

We prove the first proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together ... more >>>

ISSN 1433-8092 | Imprint