Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with DQBF:
TR16-048 | 11th March 2016
Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda

Lifting QBF Resolution Calculi to DQBF

We examine the existing Resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems Q-Resolution < IR-calc < IRM-calc, the ... more >>>

TR18-172 | 11th October 2018
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan

Building Strategies into QBF Proofs

Strategy extraction is of paramount importance for quantified Boolean formulas (QBF), both in solving and proof complexity. It extracts (counter)models for a QBF from a run of the solver resp. the proof of the QBF, thereby allowing to certify the solver's answer resp. establish soundness of the system. So far ... more >>>

TR20-036 | 9th March 2020
Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl

Strong (D)QBF Dependency Schemes via Tautology-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 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 ... more >>>

TR20-112 | 8th June 2020
Joshua Blinkhorn

Simulating DQBF Preprocessing Techniques with Resolution Asymmetric Tautologies

Dependency quantified Boolean formulas (DQBF) describe an NEXPTIME-complete generalisation of QBF, which in turn generalises SAT. QRAT is a recently proposed proof system for quantified Boolean formulas (QBF), which simulates the full suite of QBF preprocessing techniques and thus forms a uniform proof checking format for solver verification.

In this ... more >>>

ISSN 1433-8092 | Imprint