Width and size of regular resolution proofs
Alasdair Urquhart (University of Toronto)
TL;DR
This paper investigates the minimum width of regular resolution proofs, revealing that some small regular refutations necessarily involve large clauses, contrasting with known results for general resolution proofs.
Contribution
It demonstrates that certain formulas have small regular resolution proofs but require large clauses, highlighting a fundamental difference from general resolution proof complexity.
Findings
Regular resolution proofs can be small but may involve large clauses.
Contrasts with general resolution where small proofs do not require large clauses.
Provides insights into the structure and limitations of regular resolution proofs.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.