Relating size and width in variants of Q-resolution

DOI10.1016/J.IPL.2018.05.005MaRDI QIDQ1653019zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

computational complexitylower bound techniquesproof complexityQBFresolution

Mathematics Subject Classification ID

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

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

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple
• Contributions to the theory of practical quantified Boolean formula solving
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Expansion-based QBF solving versus Q-resolution
• Feasible interpolation for QBF resolution calculi
• Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
• Lower bounds: from circuits to QBF proof systems
• On Q-resolution and CDCL QBF solving
• QBF Resolution Systems and Their Proof Complexities
• Resolution for quantified Boolean formulas
• Short proofs are narrow—resolution made simple
• Towards NP-P via proof complexity and search
• Unified QBF certification and its applications

Cited in

(5)

• Lower bounds for QCDCL via formula gauge
• scientific article; zbMATH DE number 93794 (Why is no real title available?)
• Narrow proofs may be maximally long
• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
• Lower bounds for QCDCL via formula gauge

Describes a project that uses

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)