Article

Free access

Short proofs are narrow—resolution made simple

Authors:

Eli Ben-Sasson,

Avi WigdersonAuthors Info & Claims

STOC '99: Proceedings of the thirty-first annual ACM symposium on Theory of Computing

Pages 517 - 526

https://doi.org/10.1145/301250.301392

Published: 01 May 1999 Publication History

PDF eReader

References

[1]

M. L. Boner, J. L. Esteban, N. Galesi, J. Johannsen. Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems. submitted.

Google Scholar

[2]

P. Beame, R. Karp, T. Pitassi, M. Saks. On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas. Submitted.

Google Scholar

[3]

P. Beame, T. Pitassi. Simplified a~d Improved resolution lower bounds. In 37th Annual Symposium on Foundations of Computer Sciecne, pp 274-282. Burlington, VT, October 1996. IEEE.

Digital Library

Google Scholar

[4]

S. Buss, T. Pitassi. Resolution and the Weak Pigeonhole Principle. Typeset manuscript, to appear in CSL97.

Digital Library

Google Scholar

[5]

S.R. Buss, G. Turin. Resolution Proof of generalized Pigeonhole principles. In Theoretical Uomp. Sci., 62:(1988)311-317.

Digital Library

Google Scholar

[6]

M. Clegg, J. Edmonds, R Impagliazzo Using the Groebner Basis algorithm to find proofs of unsatisfiability In Proceedings of the 28th A CM symposium on Theory of Computing, 1996, pp 174-183.

Digital Library

Google Scholar

[7]

R. Celoni, W.J. Paul, R.E. Tarjan Space Bounds for a Game on Graphs. In Math. Systems Theory, 10 (1977), pp 239-251.

Google Scholar

[8]

S.A. Cook, R. Reckhow. The relative efficiency of propositional proof systems. In J. of Symbolic Logic, Voi. 44 (1979), pp. 36-50.

Google Scholar

[9]

V. Chv,~tal, E. Szemer~di Many Hard Examples for Resolution In J. of the ACM, Vol 35 No. 4, pp. 759-768.

Digital Library

Google Scholar

[10]

M. Davis, G. Logemann, D. Loveland. A Machine program for theorem proving. In Communications oj' the A CM, 5:394-397, 1962.

Digital Library

Google Scholar

[11]

A. Haken. The Intractibility of Resolution. In Theoretical Computer Science, 39 (1985), pp. 297-308.

Crossref

Google Scholar

[12]

R.Impagliazzo, P Pudl~k, J. Sgall. Lower Bounds for the Polynomial-Calculus and the Groebner Basis Algorithm. Found at Electronic Colloqium on Computational Comple~city, Reports Series 1997, Available at http://www.eccc.unitrier.de/eccc/. Technical Report TR97-042.

Google Scholar

[13]

R. Raz, P. McKenzie. Separation of the Monotone NC Hierarchy. submitted.

Google Scholar

[14]

N. Pippenger Pebbling. Technical Report, IBM Watson Research Center.

Google Scholar

[15]

A.A. Razborov Unprovability of Lower Bounds on Circuit Size in Certain Fragments of Bounded Arithmetic. Izvestia of the RAN, 59 (1), pages 201-222, 1995.

Google Scholar

[16]

A.A. Razborov, S. Rudich. Natural Proofs. In Proc. of the 26th STOC, 1994, pp. 204-213.

Digital Library

Google Scholar

[17]

A.A. Razborov, A. Wigderson, A. Yao~ Read- Once Branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus. In Proc. of the 29th STOC, 1997, pp. 739- 748.

Digital Library

Google Scholar

[18]

G.S. Tseitin On the Complexity of Derivation in Propositional Calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2. Consultants Bureau, New-York-London, 1968, pp. ! t5-125.

Google Scholar

[19]

A. Urquhart. Hard Examples for Resolution. In J. of the A CM, Vol 34 No. 1, pp. 209-219.

Digital Library

Google Scholar

[20]

A. Urquhart. The Complexity of Propositional Proofs In The Bulletin of Symbolic Logic, Vol 1 No. 4 (1995), pp. 425-467.

Crossref

Google Scholar

Cited By

View all

Impagliazzo RMouli SPitassi T(2023)Lower Bounds for Polynomial Calculus with Extension Variables over Finite FieldsProceedings of the conference on Proceedings of the 38th Computational Complexity Conference10.4230/LIPIcs.CCC.2023.7(1-24)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.4230/LIPIcs.CCC.2023.7
Hopkins MLin T(2022)Explicit Lower Bounds Against Ω(n)-Rounds of Sum-of-Squares2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS)10.1109/FOCS54457.2022.00069(662-673)Online publication date: Oct-2022
https://doi.org/10.1109/FOCS54457.2022.00069
Jamali SMitchell D(2018)Centrality-Based Improvements to CDCL HeuristicsTheory and Applications of Satisfiability Testing – SAT 201810.1007/978-3-319-94144-8_8(122-131)Online publication date: 26-Jun-2018
https://doi.org/10.1007/978-3-319-94144-8_8
Show More Cited By

Index Terms

Short proofs are narrow—resolution made simple

Recommendations

Short Proofs are Narrow - Resolution Made Simple
COCO '99: Proceedings of the Fourteenth Annual IEEE Conference on Computational Complexity

The width of a Resolution proof is defined to be the maximal number of literals in any clause of the proof. In this paper we relate proof width to proof size, in both general Resolution, and its tree-like variant. Specifically, the main observation of ...
Are Short Proofs Narrow? QBF Resolution Is Not So Simple

The ground-breaking paper “Short Proofs Are Narrow -- Resolution Made Simple” by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of ...
Short resolution proofs for a sequence of tricky formulas
Abstract
A class of propositional formulas, encoding the property that every finite, transitive digraph with no two-cycles must have a source, has been investigated by Krishnamurty and conjectured as hard for resolution. In this note we prove, opposed to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

STOC '99: Proceedings of the thirty-first annual ACM symposium on Theory of Computing

May 1999

790 pages

ISBN:1581130678

DOI:10.1145/301250

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 1999

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

STOC99

Sponsor:

SIGACT

STOC99: ACM Symposium on Theory of Computing

May 1 - 4, 1999

Georgia, Atlanta, USA

Acceptance Rates

Overall Acceptance Rate 1,469 of 4,586 submissions, 32%

Upcoming Conference

STOC '25

Sponsor:
sigact

57th Annual ACM Symposium on Theory of Computing (STOC 2025)

June 23 - 27, 2025

Prague , Czech Republic

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

45
Total Citations
View Citations
789
Total Downloads

Downloads (Last 12 months)183
Downloads (Last 6 weeks)32

Reflects downloads up to 15 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Impagliazzo RMouli SPitassi T(2023)Lower Bounds for Polynomial Calculus with Extension Variables over Finite FieldsProceedings of the conference on Proceedings of the 38th Computational Complexity Conference10.4230/LIPIcs.CCC.2023.7(1-24)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.4230/LIPIcs.CCC.2023.7
Hopkins MLin T(2022)Explicit Lower Bounds Against Ω(n)-Rounds of Sum-of-Squares2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS)10.1109/FOCS54457.2022.00069(662-673)Online publication date: Oct-2022
https://doi.org/10.1109/FOCS54457.2022.00069
Jamali SMitchell D(2018)Centrality-Based Improvements to CDCL HeuristicsTheory and Applications of Satisfiability Testing – SAT 201810.1007/978-3-319-94144-8_8(122-131)Online publication date: 26-Jun-2018
https://doi.org/10.1007/978-3-319-94144-8_8
Riazanov A(2018)On the Decision Trees with SymmetriesComputer Science – Theory and Applications10.1007/978-3-319-90530-3_24(282-294)Online publication date: 25-Apr-2018
https://doi.org/10.1007/978-3-319-90530-3_24
Lauria MPudlák PRödl VThapen N(2017)The complexity of proving that a graph is RamseyCombinatorica10.1007/s00493-015-3193-937:2(253-268)Online publication date: 1-Apr-2017
https://dl.acm.org/doi/10.1007/s00493-015-3193-9
Imanishi K(2017)An Upper Bound for Resolution Size: Characterization of Tractable SAT InstancesWALCOM: Algorithms and Computation10.1007/978-3-319-53925-6_28(359-369)Online publication date: 21-Feb-2017
https://doi.org/10.1007/978-3-319-53925-6_28
Pitassi TRossman BServedio RTan LWichs DMansour Y(2016)Poly-logarithmic Frege depth lower bounds via an expander switching lemmaProceedings of the forty-eighth annual ACM symposium on Theory of Computing10.1145/2897518.2897637(644-657)Online publication date: 19-Jun-2016
https://dl.acm.org/doi/10.1145/2897518.2897637
Daniely AWichs DMansour Y(2016)Complexity theoretic limitations on learning halfspacesProceedings of the forty-eighth annual ACM symposium on Theory of Computing10.1145/2897518.2897520(105-117)Online publication date: 19-Jun-2016
https://dl.acm.org/doi/10.1145/2897518.2897520
Applebaum BBogdanov ARosen A(2016)A Dichotomy for Local Small-Bias GeneratorsJournal of Cryptology10.1007/s00145-015-9202-829:3(577-596)Online publication date: 1-Jul-2016
https://dl.acm.org/doi/10.1007/s00145-015-9202-8
Buresh-Oppenheim JPitassi T(2014)The complexity of resolution refinementsThe Journal of Symbolic Logic10.2178/jsl/120335079072:04(1336-1352)Online publication date: 12-Mar-2014
https://doi.org/10.2178/jsl/1203350790
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Short Proofs are Narrow - Resolution Made Simple

Are Short Proofs Narrow? QBF Resolution Is Not So Simple

Short resolution proofs for a sequence of tricky formulas