Lower bound techniques for QBF expansion

DOI10.1007/s00224-019-09940-0zbMath1471.03081OpenAlexW2965133072MaRDI QIDQ1987510

Olaf Beyersdorff, Joshua Blinkhorn

Publication date: 15 April 2020

Published in: Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00224-019-09940-0

zbMATH Keywords

resolutionproof complexityQBFlower-bound techniques

Mathematics Subject Classification ID

Complexity of proofs (03F20)

Related Items (2)

A simple proof of QBF hardness ⋮ Proof complexity of symbolic QBF reasoning

Uses Software

• RAReQS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solving QBF with counterexample guided refinement
• Towards NP-P via proof complexity and search
• Resolution for quantified Boolean formulas
• Expansion-based QBF solving versus Q-resolution
• Conformant planning as a case study of incremental QBF solving
• A characterization of tree-like resolution size
• A Game Characterisation of Tree-like Q-resolution Size
• Lower Bounds
• On Stronger Calculi for QBFs
• Q-Resolution with Generalized Axioms
• Long Distance Q-Resolution with Dependency Schemes
• Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
• On Unification of QBF Resolution-Based Calculi
• QBF Resolution Systems and Their Proof Complexities
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Fault Localization and Correction with QBF
• The relative efficiency of propositional proof systems
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Short proofs are narrow—resolution made simple
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple
• Proof Complexity Modulo the Polynomial Hierarchy
• Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test
• Experiments with Reduction Finding
• The Complexity of Propositional Proofs
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

This page was built for publication: Lower bound techniques for QBF expansion