Classes of hard formulas for QBF resolution
From MaRDI portal
Publication:6488807
DOI10.1613/JAIR.1.14710MaRDI QIDQ6488807
Olaf Beyersdorff, Agnes Schleitzer
Publication date: 23 October 2023
Published in: The Journal of Artificial Intelligence Research (JAIR) (Search for Journal in Brave)
Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the power of clause-learning SAT solvers as resolution engines
- The intractability of resolution
- Minimal unsatisfiability and minimal strongly connected digraphs
- Resolution for quantified Boolean formulas
- Lower bound techniques for QBF expansion
- Building strategies into QBF proofs
- QBFFam: a tool for generating QBF families from proof complexity
- Proof complexity of fragments of long-distance Q-resolution
- Characterising tree-like Frege proofs for QBF
- Expansion-based QBF solving versus Q-resolution
- Unified QBF certification and its applications
- A simple proof of QBF hardness
- On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
- QBF Resolution Systems and Their Proof Complexities
- Hard examples for resolution
- The relative efficiency of propositional proof systems
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- Reasons for Hardness in QBF Proof Systems
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- New Resolution-Based QBF Calculi and Their Proof Complexity
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- The Complexity of Propositional Proofs
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
This page was built for publication: Classes of hard formulas for QBF resolution
