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

lower-bound techniquesproof complexityQBFseparations

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) 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

(48)

• Understanding cutting planes for QBFs
• \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
• Building strategies into QBF proofs
• QBFFam: a tool for generating QBF families from proof complexity
• Lower bounds for QCDCL via formula gauge
• Hardness and optimality in QBF proof systems modulo NP
• Proof complexity of symbolic QBF reasoning
• Proof complexity of QBF symmetry recomputation
• Proof complexity of fragments of long-distance Q-resolution
• Expansion-based QBF solving versus Q-resolution
• A simple proof of QBF hardness
• On Q-resolution and CDCL QBF solving
• On Stronger Calculi for QBFs
• Lifting QBF resolution calculi to DQBF
• On sequent systems and resolution for QBFs
• On Unification of QBF Resolution-Based Calculi
• Proof complexity of resolution-based QBF calculi
• QBF Resolution Systems and Their Proof Complexities
• NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability
• Feasible interpolation for QBF resolution calculi
• A First Step Towards a Unified Proof Checker for QBF
• Understanding cutting planes for QBFs
• Building strategies into QBF proofs
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
• Feasible interpolation for QBF resolution calculi
• On propositional QBF expansions and Q-resolution
• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
• Lower bounds for QCDCL via formula gauge
• Never trust your solver: certification for SAT and QBF
• True crafted formula families for benchmarking quantified satisfiability solvers
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
• Towards Uniform Certification in QBF
• Proof Complexity of Quantified Boolean Logic — A Survey
• Subsumption-linear Q-resolution for QBF theorem proving
• Classes of hard formulas for 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
• QBF merge resolution is powerful but unnatural
• Strategy extraction by interpolation
• Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
• Strong (D)QBF dependency schemes via implication-free resolution paths
• Hard QBFs for merge resolution
• QCDCL with cube learning or pure literal elimination -- what is best?
• Understanding the relative strength of QBF CDCL solvers and QBF resolution
• Polynomial calculus for quantified Boolean logic: lower bounds through circuits and degree
• Extending merge resolution to a family of QBF-proof systems
• On the interplay of cube learning and dependency schemes in QCDCL proof systems
• Proof complexity of modal resolution

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)