Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
From MaRDI portal
(Redirected from Publication:5886517)
Recommendations
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- Proof complexity of resolution-based QBF calculi
- New resolution-based QBF calculi and their proof complexity
- Classes of hard formulas for QBF resolution
- Hardness and optimality in QBF proof systems modulo NP
- QBF Resolution Systems and Their Proof Complexities
- scientific article; zbMATH DE number 7029312
- Size, cost and capacity: a semantic technique for hard random QBFs
- Small resolution proofs for QBF using dependency treewidth
- On Q-resolution and CDCL QBF solving
Cites work
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
- A game characterisation of tree-like Q-resolution size
- A Machine-Oriented Logic Based on the Resolution Principle
- A subexponential exact learning algorithm for DNF using equivalence queries
- Are Short Proofs Narrow? QBF Resolution Is Not So Simple
- Circuit complexity, proof complexity, and polynomial identity testing. The ideal proof system
- Conformant planning as a case study of incremental QBF solving
- Contributions to the theory of practical quantified Boolean formula solving
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- Expansion-based QBF solving versus Q-resolution
- Feasible interpolation for QBF resolution calculi
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- scientific article; zbMATH DE number 1860652 (Why is no real title available?)
- scientific article; zbMATH DE number 819737 (Why is no real title available?)
- scientific article; zbMATH DE number 7592011 (Why is no real title available?)
- Logical foundations of proof complexity
- Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
- Lower bounds: from circuits to QBF proof systems
- New resolution-based QBF calculi and their proof complexity
- On Q-resolution and CDCL QBF solving
- On the computational power of Boolean decision lists
- On the correspondence between arithmetic theories and propositional proof systems – a survey
- Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness
- Proof complexity of resolution-based QBF calculi
- Proof systems that take advice
- Q-resolution with generalized axioms
- Reasons for hardness in QBF proof systems
- Relating size and width in variants of Q-resolution
- Resolution for quantified Boolean formulas
- Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test
- Short proofs are narrow—resolution made simple
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- The Complexity of Propositional Proofs
- The intractability of resolution
- The relative efficiency of propositional proof systems
- Towards NP-P via proof complexity and search
- Understanding Gentzen and Frege Systems for QBF
- Unified QBF certification and its applications
Cited in
(9)- Unified Characterisations of Resolution Hardness Measures
- scientific article; zbMATH DE number 7228403 (Why is no real title available?)
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- Term Rewriting and Applications
- Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
- Strategy extraction by interpolation
- Hard QBFs for merge resolution
- Polynomial calculus for quantified Boolean logic: lower bounds through circuits and degree
This page was built for publication: Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5886517)
