Relating size and width in variants of Q-resolution

DOI10.1016/j.ipl.2018.05.005zbMath1458.03043OpenAlexW2804939161MaRDI QIDQ1653019

Olaf Beyersdorff, Judith Clymo

Publication date: 17 July 2018

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2018.05.005

zbMATH Keywords

computational complexityresolutionproof complexityQBFlower bound techniques

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Related Items (3)

Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ Lower bounds for QCDCL via formula gauge ⋮ Lower bounds for QCDCL via formula gauge

Uses Software

• DepQBF

Cites Work

• Unnamed Item
• Towards NP-P via proof complexity and search
• Resolution for quantified Boolean formulas
• Expansion-based QBF solving versus Q-resolution
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Unified QBF certification and its applications
• Lower Bounds
• On Q-Resolution and CDCL QBF Solving
• Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
• QBF Resolution Systems and Their Proof Complexities
• Short proofs are narrow—resolution made simple
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple
• Contributions to the Theory of Practical Quantified Boolean Formula Solving
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving

This page was built for publication: Relating size and width in variants of Q-resolution