A simple proof of QBF hardness
From MaRDI portal
Publication:2656352
DOI10.1016/J.IPL.2021.106093OpenAlexW3119804017MaRDI QIDQ2656352FDOQ2656352
Authors: Olaf Beyersdorff, Joshua Blinkhorn
Publication date: 11 March 2021
Published in: Information Processing Letters (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ipl.2021.106093
Cites Work
- Resolution for quantified Boolean formulas
- Expansion-based QBF solving versus Q-resolution
- On Unification of QBF Resolution-Based Calculi
- Proof complexity of resolution-based QBF calculi
- Title not available (Why is that?)
- Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
- QBF Resolution Systems and Their Proof Complexities
- A Machine-Oriented Logic Based on the Resolution Principle
- The intractability of resolution
- On the power of clause-learning SAT solvers as resolution engines
- The Complexity of Propositional Proofs
- Frege systems for quantified Boolean logic
- A game characterisation of tree-like Q-resolution size
- Title not available (Why is that?)
- Proof Complexity
- Title not available (Why is that?)
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- New resolution-based QBF calculi and their proof complexity
- On Q-resolution and CDCL QBF solving
- Short proofs for some symmetric quantified Boolean formulas
- Lower bound techniques for QBF expansion
- Q-resolution with generalized axioms
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
Cited In (7)
- Are Short Proofs Narrow? QBF Resolution is not Simple.
- Classes of hard formulas for QBF resolution
- QBF as an alternative to Courcelle's theorem
- Are Short Proofs Narrow? QBF Resolution Is Not So Simple
- Short proofs in QBF expansion
- Title not available (Why is that?)
- QBFFam: a tool for generating QBF families from proof complexity
Uses Software
This page was built for publication: A simple proof of QBF hardness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2656352)