Classes of hard formulas for QBF resolution
DOI10.1613/JAIR.1.14710MaRDI QIDQ6488807FDOQ6488807
Authors: Agnes Schleitzer, Olaf Beyersdorff 
Publication date: 23 October 2023
Published in: The Journal of Artificial Intelligence Research (JAIR) (Search for Journal in Brave)
Recommendations
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)
Cites Work
- Resolution for quantified Boolean formulas
- Expansion-based QBF solving versus Q-resolution
- Unified QBF certification and its applications
- Contributions to the theory of practical quantified Boolean formula solving
- 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
- Hard examples for resolution
- Logical foundations of proof complexity
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- Title not available (Why is that?)
- The relative efficiency of propositional proof systems
- The intractability of resolution
- On the power of clause-learning SAT solvers as resolution engines
- The Complexity of Propositional Proofs
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
- On the relative complexity of resolution refinements and cutting planes proof systems
- 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
- QBFFam: a tool for generating QBF families from proof complexity
- Minimal unsatisfiability and minimal strongly connected digraphs
- Characterising tree-like Frege proofs for QBF
- A simple proof of QBF hardness
- Lower bound techniques for QBF expansion
- Building strategies into QBF proofs
- Proof complexity of fragments of long-distance Q-resolution
- Reasons for hardness in QBF proof systems
Cited In (4)
This page was built for publication: Classes of hard formulas for QBF resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6488807)
