A Game Characterisation of Tree-like Q-resolution Size

DOI10.1007/978-3-319-15579-1_38zbMath1425.03027WikidataQ61835452 ScholiaQ61835452MaRDI QIDQ2799200

Leroy Chew, Karteek Sreenivasaiah, Olaf Beyersdorff

Publication date: 8 April 2016

Published in: Language and Automata Theory and Applications (Search for Journal in Brave)

Full work available at URL: http://eprints.whiterose.ac.uk/85649/1/paper.pdf

Mathematics Subject Classification ID

68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

03F20: Complexity of proofs

Related Items

Unnamed Item, Unnamed Item, Unnamed Item, Understanding cutting planes for QBFs, Lower bound techniques for QBF expansion, A game characterisation of tree-like Q-resolution size, Feasible Interpolation for QBF Resolution Calculi

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Towards NP-P via proof complexity and search
• A combinatorial characterization of treelike resolution space
• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
• Resolution for quantified Boolean formulas
• Unified QBF certification and its applications
• A characterization of tree-like resolution size
• A combinatorial characterization of resolution width
• Proofs as Games
• On Sequent Systems and Resolution for QBFs
• Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
• On Unification of QBF Resolution-Based Calculi
• Lower bounds for bounded depth Frege proofs via Pudlák-Buss games
• QBF Resolution Systems and Their Proof Complexities
• Unified Characterisations of Resolution Hardness Measures
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Short proofs are narrow—resolution made simple
• Contributions to the Theory of Practical Quantified Boolean Formula Solving
• On Propositional QBF Expansions and Q-Resolution
• The Complexity of Propositional Proofs
• Parameterized Complexity of DPLL Search Procedures