New resolution-based QBF calculi and their proof complexity

DOI10.1145/3352155MaRDI QIDQ5205822zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

QBFproof complexityseparationslower-bound techniques

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)

Recommendations

• Proof complexity of resolution-based QBF calculi
• On Unification of QBF Resolution-Based Calculi
• QBF Resolution Systems and Their Proof Complexities
• Expansion-based QBF solving versus Q-resolution
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple

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
• Hardness and optimality in QBF proof systems modulo NP
• Lower bounds for QCDCL via formula gauge
• Proof complexity of QBF symmetry recomputation
• Towards Uniform Certification in QBF
• Feasible interpolation for QBF resolution calculi
• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
• Lifting QBF resolution calculi to DQBF
• Proof complexity of resolution-based QBF calculi
• On propositional QBF expansions and Q-resolution
• Building strategies into QBF proofs
• Classes of hard formulas for QBF resolution
• Proof complexity of fragments of long-distance Q-resolution
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
• Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
• 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
• On Q-resolution and CDCL QBF solving
• On sequent systems and resolution for QBFs
• Understanding cutting planes for QBFs
• Proof complexity of symbolic QBF reasoning
• QBF merge resolution is powerful but unnatural
• Subsumption-linear Q-resolution for QBF theorem proving
• 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
• QBFFam: a tool for generating QBF families from proof complexity
• 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

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)