Classes of hard formulas for QBF resolution

DOI10.1613/JAIR.1.14710MaRDI QIDQ6488807zbMATH OpenFDO

Authors Agnes Schleitzer, Olaf Beyersdorff

Publication date 23 October 2023

Published in The Journal of Artificial Intelligence Research (JAIR) (Search for Journal in Brave)

zbMATH Keywords

satisfiabilitytheorem proving

Mathematics Subject Classification ID

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)

Recommendations

• New resolution-based QBF calculi and their proof complexity
• Proof complexity of resolution-based QBF calculi
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
• Reasons for hardness in QBF proof systems
• On sequent systems and resolution for QBFs

Cites work

• scientific article; zbMATH DE number 5595151 (Why is no real title available?)
• scientific article; zbMATH DE number 7029312 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• A simple proof of QBF hardness
• Building strategies into QBF proofs
• Characterising tree-like Frege proofs for QBF
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Contributions to the theory of practical quantified Boolean formula solving
• Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
• Expansion-based QBF solving versus Q-resolution
• Hard examples for resolution
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
• Logical foundations of proof complexity
• Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
• Lower bound techniques for QBF expansion
• Minimal unsatisfiability and minimal strongly connected digraphs
• New resolution-based QBF calculi and their proof complexity
• On the power of clause-learning SAT solvers as resolution engines
• On the relative complexity of resolution refinements and cutting planes proof systems
• Proof complexity of fragments of long-distance Q-resolution
• QBF Resolution Systems and Their Proof Complexities
• QBFFam: a tool for generating QBF families from proof complexity
• Reasons for hardness in QBF proof systems
• Resolution for quantified Boolean formulas
• The Complexity of Propositional Proofs
• The intractability of resolution
• The relative efficiency of propositional proof systems
• Unified QBF certification and its applications

Cited in

(4)

• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
• QBF Resolution Systems and Their Proof Complexities
• scientific article; zbMATH DE number 7278086 (Why is no real title available?)
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution

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)