Name
Abstract | ||
|---|---|---|
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 expansion DQBF system \\(\\mathsf {\\forall {Exp{\\text{+ }}Res}}\\). |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/978-3-030-51825-7_28 | Electronic Colloquium on Computational Complexity (ECCC) |
DocType | Volume | Citations |
Journal | 27 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Olaf Beyersdorff | 1 | 223 | 30.33 |
| Joshua Blinkhorn | 2 | 3 | 6.16 |
| Tomás Peitl | 3 | 6 | 4.82 |