QBF Resolution Systems and Their Proof Complexities
From MaRDI portal
Recommendations
- Proof complexity of resolution-based QBF calculi
- New resolution-based QBF calculi and their proof complexity
- On sequent systems and resolution for QBFs
- Proof complexity of symbolic QBF reasoning
- Classes of hard formulas for QBF resolution
- A resolution-style proof system for DQBF
- Computer Science Logic
- On propositional QBF expansions and Q-resolution
- Hardness and optimality in QBF proof systems modulo NP
Cited in
(58)- Q-resolution with generalized axioms
- Long distance Q-resolution with dependency schemes
- Lower bound techniques for QBF expansion
- The QBF Gallery: behind the scenes
- Understanding Gentzen and Frege Systems for QBF
- Quantified maximum satisfiability
- Functional synthesis via input-output separation
- Lower bounds for QCDCL via formula gauge
- Towards Uniform Certification in QBF
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- New resolution-based QBF calculi and their proof complexity
- Lifting QBF resolution calculi to DQBF
- Are Short Proofs Narrow? QBF Resolution is not Simple.
- Strong (D)QBF dependency schemes via implication-free resolution paths
- Hard QBFs for merge resolution
- Building strategies into QBF proofs
- Classes of hard formulas for QBF resolution
- Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
- A game characterisation of tree-like Q-resolution size
- Relating size and width in variants of Q-resolution
- QBF as an alternative to Courcelle's theorem
- Understanding the relative strength of QBF CDCL solvers and QBF resolution
- Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
- Antichain-Based QBF Solving
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
- Understanding cutting planes for QBFs
- Polynomial calculus for quantified Boolean logic: lower bounds through circuits and degree
- On Q-resolution and CDCL QBF solving
- Unified QBF certification and its applications
- Proof complexity of symbolic QBF reasoning
- QBF merge resolution is powerful but unnatural
- Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable
- On Unification of QBF Resolution-Based Calculi
- scientific article; zbMATH DE number 7228403 (Why is no real title available?)
- Models and counter-models of quantified Boolean formulas (invited talk)
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- Short proofs for some symmetric quantified Boolean formulas
- Lower bounds for QCDCL via formula gauge
- Theory and Applications of Satisfiability Testing
- A game characterisation of tree-like Q-resolution size
- Feasible interpolation for QBF resolution calculi
- Size, cost and capacity: a semantic technique for hard random QBFs
- A simple proof of QBF hardness
- On QBF Proofs and Preprocessing
- On Stronger Calculi for QBFs
- Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs
- Lower bound techniques for QBF proof systems
- Are Short Proofs Narrow? QBF Resolution Is Not So Simple
- Long-distance Q-resolution with dependency schemes
- HordeQBF: a modular and massively parallel QBF solver
- Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms
- QBFFam: a tool for generating QBF families from proof complexity
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- scientific article; zbMATH DE number 7278086 (Why is no real title available?)
- 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: QBF Resolution Systems and Their Proof Complexities
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192061)
