Relating size and width in variants of Q-resolution

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

Authors: Judith Clymo, Olaf Beyersdorff 

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

Recommendations

• Are Short Proofs Narrow? QBF Resolution is not Simple.
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple
• Short proofs are narrow—resolution made simple
• Optimality of size-width tradeoffs for resolution
• Short proofs are narrow -- resolution made simple

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

• 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
• Feasible interpolation for QBF resolution calculi
• Lower bounds: from circuits to QBF proof systems
• On Q-resolution and CDCL QBF solving

Cited In (5)

• 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
• Narrow proofs may be maximally long

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)