Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
From MaRDI portal
Publication:5886517
DOI10.1145/3565286OpenAlexW3013210104MaRDI QIDQ5886517
Joshua Blinkhorn, Tomáš Peitl, Olaf Beyersdorff, Meena Mahajan
Publication date: 5 April 2023
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/3565286
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Towards NP-P via proof complexity and search
- Proof systems that take advice
- On the computational power of Boolean decision lists
- The intractability of resolution
- Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
- Relating size and width in variants of Q-resolution
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
- A subexponential exact learning algorithm for DNF using equivalence queries
- Resolution for quantified Boolean formulas
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- Expansion-based QBF solving versus Q-resolution
- Conformant planning as a case study of incremental QBF solving
- A game characterisation of tree-like Q-resolution size
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- Unified QBF certification and its applications
- Lower Bounds
- On Q-Resolution and CDCL QBF Solving
- Q-Resolution with Generalized Axioms
- On the correspondence between arithmetic theories and propositional proof systems – a survey
- The relative efficiency of propositional proof systems
- Short proofs are narrow—resolution made simple
- Are Short Proofs Narrow? QBF Resolution Is Not So Simple
- Circuit Complexity, Proof Complexity, and Polynomial Identity Testing
- Understanding Gentzen and Frege Systems for QBF
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- Proof Complexity Modulo the Polynomial Hierarchy
- Reasons for Hardness in QBF Proof Systems
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- New Resolution-Based QBF Calculi and Their Proof Complexity
- Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- The Complexity of Propositional Proofs
- A Machine-Oriented Logic Based on the Resolution Principle
This page was built for publication: Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
