New resolution-based QBF calculi and their proof complexity
DOI10.1145/3352155zbMATH Open1496.68362OpenAlexW2972754151WikidataQ127239097 ScholiaQ127239097MaRDI QIDQ5205822FDOQ5205822
Authors: Olaf Beyersdorff, Leroy Chew, Mikoláš Janota 
Publication date: 16 December 2019
Published in: ACM Transactions on Computation Theory (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/3352155
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)
Cited In (38)
- A First Step Towards a Unified Proof Checker for QBF
- Proof Complexity of Quantified Boolean Logic — A Survey
- Proof complexity of modal resolution
- Towards Uniform Certification in QBF
- Hardness and optimality in QBF proof systems modulo NP
- Lower bounds for QCDCL via formula gauge
- Proof complexity of QBF symmetry recomputation
- Feasible interpolation for QBF resolution calculi
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- On propositional QBF expansions and Q-resolution
- Lifting QBF resolution calculi to DQBF
- Proof complexity of resolution-based QBF calculi
- Classes of hard formulas for QBF resolution
- Building strategies into QBF proofs
- Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
- Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
- Proof complexity of fragments of long-distance Q-resolution
- Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
- Expansion-based QBF solving versus Q-resolution
- Understanding cutting planes for QBFs
- Understanding cutting planes for QBFs
- On Q-resolution and CDCL QBF solving
- On sequent systems and resolution for QBFs
- QBF merge resolution is powerful but unnatural
- Subsumption-linear Q-resolution for QBF theorem proving
- Proof complexity of symbolic QBF reasoning
- On Unification of QBF Resolution-Based Calculi
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
- Lower bounds for QCDCL via formula gauge
- NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability
- Feasible interpolation for QBF resolution calculi
- A simple proof of QBF hardness
- On Stronger Calculi for QBFs
- QBF Resolution Systems and Their Proof Complexities
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- Never trust your solver: certification for SAT and QBF
- True crafted formula families for benchmarking quantified satisfiability solvers
- QBFFam: a tool for generating QBF families from proof complexity
This page was built for publication: New resolution-based QBF calculi and their proof complexity
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5205822)
