research-article

Strong ETH holds for regular resolution

Authors:

Christopher Beck,

Russell ImpagliazzoAuthors Info & Claims

STOC '13: Proceedings of the forty-fifth annual ACM symposium on Theory of Computing

Pages 487 - 494

https://doi.org/10.1145/2488608.2488669

Published: 01 June 2013 Publication History

Abstract

We obtain asymptotically sharper lower bounds on resolution complexity for k-CNF's than was known previously. We show that for any large enough k there are k-CNF's which require resolution width (1-~O(k^-1/4))n, regular resolution size 2^{(1-~O(k^-1/4))n}, and general resolution size (3/2)^{(1-~O(k^-1/4))n}.

References

[1]

P. Beame, C. Beck, and R. Impagliazzo. Time-space tradeoffs in resolution: Superpolynomial lower bounds for superlinear space. In Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC '12), pages 213--232, May 2012.

Digital Library

[2]

P. W. Beame and T. Pitassi. Simplified and improved resolution lower bounds. In Proceedings 37th Annual Symposium on Foundations of Computer Science, pages 274--282, Burlington, VT, Oct. 1996. IEEE.

Digital Library

[3]

E. Ben-Sasson and R. Impagliazzo. Random CNF's are hard for the polynomial calculus. In Proceedings 40th Annual Symposium on Foundations of Computer Science, pages 415--421, New York,NY, Oct. 1999. IEEE.

Digital Library

[4]

E. Ben-Sasson and A. Wigderson. Short proofs are narrow -- resolution made simple. In Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing, pages 517--526, Atlanta, GA, May 1999.

Digital Library

[5]

S. Buss, D. Grigoriev, R. Impagliazzo, and T. Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. In Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing, pages 547--556, Atlanta, GA, May 1999.

Digital Library

[6]

V. Chvátal and E. Szemerédi. Many hard examples for resolution. Journal of the ACM, 35(4):759--768, Oct. 1988.

Digital Library

[7]

M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394--397, July 1962.

Digital Library

[8]

M. Davis and H. Putnam. A computing procedure for quantification theory. Communications of the ACM, 7:201--215, 1960.

Digital Library

[9]

Z. Galil. On the complexity of regular resolution and the Davis-Putnam procedure. Theoretical Computer Science, 4:23--46, 1977.

[10]

D. Grigoriev. Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity. Theoretical Computer Science, 259:613--622, 2001.

Digital Library

[11]

L. K. Grover. A fast quantum mechanical algorithm for database search. In G. L. Miller, editor, STOC, pages 212--219. ACM, 1996.

Digital Library

[12]

A. Haken. The intractability of resolution. Theoretical Computer Science, 39:297--305, 1985.

[13]

A. Haken and S. A. Cook. An exponential lower bound for the size of monotone real circuits. Journal of Computer and System Sciences, 58:326--335, 1999.

Digital Library

[14]

T. Hertli. 3-sat faster and simpler - unique-sat bounds for ppsz hold in general. In R. Ostrovsky, editor, FOCS, pages 277--284. IEEE, 2011.

Digital Library

[15]

R. Impagliazzo, W. Matthews, and R. Paturi. A satisfiability algorithm for ac0. In Y. Rabani, editor, SODA, pages 961--972. SIAM, 2012.

Digital Library

[16]

R. Impagliazzo and R. Paturi. On the complexity of k-SAT. Journal of Computer and System Sciences, 67:367--375, 2001.

Digital Library

[17]

R. Impagliazzo, P. Pudlák, and J. Sgall. Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Computational Complexity, 8(2):127--144, 1999.

Digital Library

[18]

R. Paturi, P. Pudlák, M. E. Saks, and F. Zane. An improved exponential-time algorithm for k-sat. J. ACM, 52(3):337--364, 2005.

Digital Library

[19]

R. Paturi, P. Pudlák, and F. Zane. Satisfiability coding lemma. In FOCS, pages 566--574. IEEE Computer Society, 1997.

Digital Library

[20]

P. Pudlák and R. Impagliazzo. A lower bound for dll algorithms for k-sat (preliminary version). In D. B. Shmoys, editor, SODA, pages 128--136. ACM/SIAM, 2000.

Digital Library

[21]

R. Raz. Resolution lower bounds for the weak pigeonhole principle. In Proceedings of the Thirty-Fourth Annual ACM Symposium on Theory of Computing, pages 553--562, Montreal, Quebec, Canada, May 2002.

Digital Library

[22]

A. A. Razborov. Improved resolution lower bounds for the weak pigeonhole principle. Technical Report TR01-055, Electronic Colloquium in Computation Complexity, http://www.eccc.uni-trier.de/eccc/, 2001.

[23]

A. A. Razborov. Resolution lower bounds for the weak functional pigeonhole principle. Technical Report TR01-075, Electronic Colloquium in Computation Complexity, http://www.eccc.uni-trier.de/eccc/, 2001.

[24]

J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23--41, Jan. 1965.

Digital Library

[25]

The international SAT Competitions. http://www.satcompetition.org.

[26]

G. Schoenebeck. Linear level lasserre lower bounds for certain k-csps. In FOCS, pages 593--602. IEEE Computer Society, 2008.

Digital Library

[27]

U. Schöning. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In Proceedings 40th Annual Symposium on Foundations of Computer Science, pages 410--414, New York,NY, Oct. 1999. IEEE.

Digital Library

[28]

J. Simon and S.-C. Tsai. On the bottleneck counting argument. Theor. Comput. Sci., 237(1--2):429--437, 2000.

Digital Library

[29]

G. Tseitin. On the complexity of derivation in propositional calculus. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning, pages 466--483. Springer, Berlin, 1983.

[30]

A. Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209--219, Jan. 1987.

Digital Library

[31]

R. Williams. Non-uniform acc circuit lower bounds. In IEEE Conference on Computational Complexity, pages 115--125. IEEE Computer Society, 2011.

Digital Library

Cited By

Abboud ABringmann KHermelin DShabtay D(2022)SETH-based Lower Bounds for Subset Sum and Bicriteria PathACM Transactions on Algorithms10.1145/345052418:1(1-22)Online publication date: 23-Jan-2022
https://dl.acm.org/doi/10.1145/3450524
de Colnet AMengel S(2021)Characterizing Tseitin-Formulas with Short Regular Resolution RefutationsTheory and Applications of Satisfiability Testing – SAT 202110.1007/978-3-030-80223-3_9(116-133)Online publication date: 2-Jul-2021
https://doi.org/10.1007/978-3-030-80223-3_9
Dalzell AHarrow AKoh DLa Placa R(2020)How many qubits are needed for quantum computational supremacy?Quantum10.22331/q-2020-05-11-2644(264)Online publication date: 11-May-2020
https://doi.org/10.22331/q-2020-05-11-264
Show More Cited By

Index Terms

Strong ETH holds for regular resolution
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
  2. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation

Recommendations

Lower Bounds for Regular Resolution over Parities
STOC 2024: Proceedings of the 56th Annual ACM Symposium on Theory of Computing

The proof system resolution over parities (Res(⊕)) operates with disjunctions of linear equations (linear clauses) over GF(2); it extends the resolution proof system by incorporating linear algebra over GF(2). Over the years, several exponential lower ...
Resolution with Counting: Dag-Like Lower Bounds and Different Moduli
Abstract
Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted $Res ({lin}_{R})$ , this refutation system operates with disjunctions of linear equations with ... $_{}$
$_{}^{}^{}_{}$
$_{}$ $_{}$ $_{}$ $_{}$
On the Relative Strength of Pebbling and Resolution

The last decade has seen a revival of interest in pebble games in the context of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing bounds on ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

STOC '13: Proceedings of the forty-fifth annual ACM symposium on Theory of Computing

June 2013

998 pages

ISBN:9781450320290

DOI:10.1145/2488608

General Chairs:
Dan Boneh
Stanford University, USA
,
Tim Roughgarden
Stanford University, USA
,
Program Chair:
Joan Feigenbaum
Yale University, USA

Copyright © 2013 ACM.

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]

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 June 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

STOC'13

Sponsor:

SIGACT

STOC'13: Symposium on Theory of Computing

June 1 - 4, 2013

California, Palo Alto, USA

Acceptance Rates

STOC '13 Paper Acceptance Rate 100 of 360 submissions, 28%;

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
343
Total Downloads

Downloads (Last 12 months)14
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Abboud ABringmann KHermelin DShabtay D(2022)SETH-based Lower Bounds for Subset Sum and Bicriteria PathACM Transactions on Algorithms10.1145/345052418:1(1-22)Online publication date: 23-Jan-2022
https://dl.acm.org/doi/10.1145/3450524
de Colnet AMengel S(2021)Characterizing Tseitin-Formulas with Short Regular Resolution RefutationsTheory and Applications of Satisfiability Testing – SAT 202110.1007/978-3-030-80223-3_9(116-133)Online publication date: 2-Jul-2021
https://doi.org/10.1007/978-3-030-80223-3_9
Dalzell AHarrow AKoh DLa Placa R(2020)How many qubits are needed for quantum computational supremacy?Quantum10.22331/q-2020-05-11-2644(264)Online publication date: 11-May-2020
https://doi.org/10.22331/q-2020-05-11-264
Abboud ABringmann KHermelin DShabtay DChan T(2019)SETH-based lower bounds for subset sum and bicriteria pathProceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms10.5555/3310435.3310438(41-57)Online publication date: 6-Jan-2019
https://dl.acm.org/doi/10.5555/3310435.3310438
Bonacina ITalebanfard N(2017)Strong ETH and Resolution via Games and the Multiplicity of StrategiesAlgorithmica10.1007/s00453-016-0228-679:1(29-41)Online publication date: 1-Sep-2017
https://dl.acm.org/doi/10.1007/s00453-016-0228-6
Williams R(2016)Strong ETH breaks with Merlin and ArthurProceedings of the 31st Conference on Computational Complexity10.5555/2982445.2982447(1-17)Online publication date: 29-May-2016
https://dl.acm.org/doi/10.5555/2982445.2982447
Abboud AHansen TWilliams VWilliams RWichs DMansour Y(2016)Simulating branching programs with edit distance and friends: or: a polylog shaved is a lower bound madeProceedings of the forty-eighth annual ACM symposium on Theory of Computing10.1145/2897518.2897653(375-388)Online publication date: 19-Jun-2016
https://dl.acm.org/doi/10.1145/2897518.2897653
Carmosino MGao JImpagliazzo RMihajlin IPaturi RSchneider SSudan M(2016)Nondeterministic Extensions of the Strong Exponential Time Hypothesis and Consequences for Non-reducibilityProceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science10.1145/2840728.2840746(261-270)Online publication date: 14-Jan-2016
https://dl.acm.org/doi/10.1145/2840728.2840746
Bonacina ITalebanfard N(2016)Improving resolution width lower bounds for k-CNFs with applications to the Strong Exponential Time HypothesisInformation Processing Letters10.1016/j.ipl.2015.09.013116:2(120-124)Online publication date: 1-Feb-2016
https://dl.acm.org/doi/10.1016/j.ipl.2015.09.013
Mikša MNordström J(2014)Long Proofs of (Seemingly) Simple FormulasTheory and Applications of Satisfiability Testing – SAT 201410.1007/978-3-319-09284-3_10(121-137)Online publication date: 2014
https://doi.org/10.1007/978-3-319-09284-3_10

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents