Lower bound techniques for QBF expansion
type: Item
instance of: scholarly article
title: Lower bound techniques for QBF expansion
zbMATH Open document ID: 1471.03081
author: Olaf Beyersdorff
author: Joshua Blinkhorn
published in: Theory of Computing Systems
publication date: 2020-04-15T00:00:00Z
review text: The article is well organized, written, and very clear. It proposes a genuine extraction strategy techniques for proving lower bounds in expansion-based QBF proof systems. It shows that the strategy size is an absolute proof-size lower bound in \(\forall\)Exp+Res, and the refined version of that strategy, i.e., the one based on the weight of the extracted strategy is an absolute proof-size lower bound in IR-calc. Besides, the authors prove an exponential IR-calc lower bound for a new class of PCNF family formulas. Finally, it shows that in the absence of propositional hardness formulas separating IR-cal and \(\forall\)Exp+Res must be \(unbounded\) quantifier alternations. Some typos: on page 407 and 415, paragraph 2 on both pages. To conclude, in the proof of Proposition 1, paragraph 1, there is a typo, instead of ``We prove the lemma'' it should be ``We prove the proposition'', and there is another typo in the proof of Proposition 2, paragraph 4, instead of ``We hence prove the lemma'' it should be ``We hence prove the proposition''.
reviewed by: Ariel Germán Fernández
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 7189478
zbMATH Keywords: QBF
zbMATH Keywords: proof complexity
zbMATH Keywords: lower-bound techniques
zbMATH Keywords: resolution
describes a project that uses: RAReQS
MaRDI profile type: Publication
full work available at URL: s00224-019-09940-0
OpenAlex ID: W2965133072
cites work: QBF Resolution Systems and Their Proof Complexities
cites work: Short proofs are narrow—resolution made simple
cites work: Q3620436
cites work: Q3304106
cites work: Q4625702
cites work: Lower bounds: from circuits to QBF proof systems
cites work: On Unification of QBF Resolution-Based Calculi
cites work: Q2954985
cites work: Q5270089
cites work: Are Short Proofs Narrow? QBF Resolution Is Not So Simple
cites work: A Game Characterisation of Tree-like Q-resolution Size
cites work: A characterization of tree-like resolution size
cites work: Q5136303
cites work: Towards NP-P via proof complexity and search
cites work: Q3457218
cites work: Proof Complexity Modulo the Polynomial Hierarchy
cites work: Q5306365
cites work: The relative efficiency of propositional proof systems
cites work: Linear reasoning. A new form of the Herbrand-Gentzen theorem
cites work: On Stronger Calculi for QBFs
cites work: Conformant planning as a case study of incremental QBF solving
cites work: Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
cites work: Q5503674
cites work: Theory and Applications of Satisfiability Testing
cites work: Solving QBF with counterexample guided refinement
cites work: Expansion-based QBF solving versus Q-resolution
cites work: Experiments with Reduction Finding
cites work: Resolution for quantified Boolean formulas
cites work: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
cites work: Q4856172
cites work: Q-Resolution with Generalized Axioms
cites work: Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test
cites work: Long Distance Q-Resolution with Dependency Schemes
cites work: Q4952609
cites work: The Complexity of Propositional Proofs
cites work: Fault Localization and Correction with QBF
cites work: Q4131648
DOI: 10.1007/S00224-019-09940-0
description: scientific article; zbMATH DE number 7189478