Proof complexity of resolution-based QBF calculi
From MaRDI portal
Recommendations
Cited in
(49)- QBF as an alternative to Courcelle's theorem
- Shortening QBF proofs with dependency schemes
- Understanding cutting planes for QBFs
- Short proofs for some symmetric quantified Boolean formulas
- Lower bound techniques for QBF expansion
- How QBF expansion makes strategy extraction hard
- Hardness and optimality in QBF proof systems modulo NP
- Proof complexity of QBF symmetry recomputation
- Proof complexity of fragments of long-distance Q-resolution
- Characterising tree-like Frege proofs for QBF
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
- Conformant planning as a case study of incremental QBF solving
- Long-distance Q-resolution with dependency schemes
- A game characterisation of tree-like Q-resolution size
- Solving QBF with counterexample guided refinement
- A simple proof of QBF hardness
- On Stronger Calculi for QBFs
- Q-resolution with generalized axioms
- Lifting QBF resolution calculi to DQBF
- Long distance Q-resolution with dependency schemes
- On sequent systems and resolution for QBFs
- The QBF Gallery: behind the scenes
- On QBF Proofs and Preprocessing
- On Unification of QBF Resolution-Based Calculi
- QBF Resolution Systems and Their Proof Complexities
- Lower bound techniques for QBF proof systems
- scientific article; zbMATH DE number 7228403 (Why is no real title available?)
- Feasible interpolation for QBF resolution calculi
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- scientific article; zbMATH DE number 1765669 (Why is no real title available?)
- Are Short Proofs Narrow? QBF Resolution is not Simple.
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- Understanding cutting planes for QBFs
- Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness
- Size, cost and capacity: a semantic technique for hard random QBFs
- On exponential lower bounds for partially ordered resolution
- CAQE and QuAbS: Abstraction Based QBF Solvers
- Reasons for hardness in QBF proof systems
- Building strategies into QBF proofs
- scientific article; zbMATH DE number 7278086 (Why is no real title available?)
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- New resolution-based QBF calculi and their proof complexity
- Feasible interpolation for QBF resolution calculi
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
- Proof Complexity of Quantified Boolean Logic — A Survey
- Classes of hard formulas for QBF resolution
- Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable
This page was built for publication: Proof complexity of resolution-based QBF calculi
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2954985)
