A game characterisation of tree-like Q-resolution size
From MaRDI portal
Publication:2424676
DOI10.1016/j.jcss.2016.11.011zbMath1425.03028OpenAlexW2570844665WikidataQ61835449 ScholiaQ61835449MaRDI QIDQ2424676
Leroy Chew, Karteek Sreenivasaiah, Olaf Beyersdorff
Publication date: 25 June 2019
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jcss.2016.11.011
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)
Related Items (7)
Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ Proof complexity of modal resolution ⋮ A simple proof of QBF hardness ⋮ Special issue: Selected papers of the 9th international conference on language and automata theory and applications, LATA 2015 ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Lower bounds for QCDCL via formula gauge ⋮ Lower bounds for QCDCL via formula gauge
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
- Expansion-based QBF solving versus Q-resolution
- Unified QBF certification and its applications
- A characterization of tree-like resolution size
- A combinatorial characterization of resolution width
- Proofs as Games
- A Game Characterisation of Tree-like Q-resolution Size
- Lower Bounds
- On Q-Resolution and CDCL QBF Solving
- On Sequent Systems and Resolution for QBFs
- Conflict-Driven XOR-Clause Learning
- 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
- Feasible Interpolation for QBF Resolution Calculi
- Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Short proofs are narrow—resolution made simple
- Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
- Are Short Proofs Narrow? QBF Resolution is not Simple.
- Understanding Gentzen and Frege Systems for QBF
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- The Complexity of Propositional Proofs
- Parameterized Complexity of DPLL Search Procedures
This page was built for publication: A game characterisation of tree-like Q-resolution size
