Hardness Characterisations and Size-width Lower Bounds for QBF Resolution

DOI10.1145/3565286MaRDI 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

zbMATH Keywords

proof complexity; quantified Boolean formulas; size-width tradeoff

Mathematics Subject Classification ID

03B70: Logic in computer science

68-XX: Computer science

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