Width and size of regular resolution proofs

DOI10.2168/LMCS-8(2:8)2012MaRDI QIDQ2888509zbMATH OpenOpenAlexFDO

Authors Alasdair Urquhart

Publication date 1 June 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1205.1050

zbMATH Keywords

regular resolution proofssize of proofswidth of proofs

Mathematics Subject Classification ID

Complexity of proofs (03F20)

Abstract: This paper discusses the topic of the minimum width of a regular resolution refutation of a set of clauses. The main result shows that there are examples having small regular resolution refutations, for which any regular refutation must contain a large clause. This forms a contrast with corresponding results for general resolution refutations.

Recommendations

• Width versus size in resolution proofs
• Theory and Applications of Models of Computation
• Short proofs are narrow—resolution made simple
• Narrow proofs may be spacious: separating space and width in resolution
• A tradeoff between length and width in resolution

Cited in

(6)

• Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
• A near-optimal separation of regular and general resolution
• Regular and General Resolution: An Improved Separation
• Hard examples for resolution
• A Logical Autobiography
• Theory and Applications of Models of Computation

This page was built for publication: Width and size of regular resolution proofs

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