Relating size and width in variants of Q-resolution

DOI10.1016/J.IPL.2018.05.005zbMATH Open1458.03043OpenAlexW2804939161WikidataQ129803932 ScholiaQ129803932MaRDI QIDQ1653019FDOQ1653019

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 complexityQBFresolutionproof complexitylower bound techniques

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

• Lower bounds for QCDCL via formula gauge
• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
• Title not available (Why is that?)
• Lower bounds for QCDCL via formula gauge

Uses Software

• DepQBF

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1653019)