research-article

A Framework for Space Complexity in Algebraic Proof Systems

Authors:

Ilario Bonacina,

Nicola GalesiAuthors Info & Claims

Journal of the ACM (JACM), Volume 62, Issue 3

Article No.: 23, Pages 1 - 20

https://doi.org/10.1145/2699438

Published: 30 June 2015 Publication History

Abstract

Algebraic proof systems, such as Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR), refute contradictions using polynomials. Space complexity for such systems measures the number of distinct monomials to be kept in memory while verifying a proof. We introduce a new combinatorial framework for proving space lower bounds in algebraic proof systems. As an immediate application, we obtain the space lower bounds previously provided for PC/PCR [Alekhnovich et al. 2002; Filmus et al. 2012]. More importantly, using our approach in its full potential, we prove Ω(n) space lower bounds in PC/PCR for random k-CNFs (k≥ 4) in n variables, thus solving an open problem posed in Alekhnovich et al. [2002] and Filmus et al. [2012]. Our method also applies to the Graph Pigeonhole Principle, which is a variant of the Pigeonhole Principle defined over a constant (left) degree expander graph.

References

[1]

Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. 2002. Space complexity in propositional calculus. SIAM J. Comput. 31, 4, 1184--1211.

Digital Library

[2]

Michael Alekhnovich and Alexander A. Razborov. 2003. Lower bounds for polynomial calculus: Non-binomial case. In Proceedings of the Steklov Institute of Mathematics, Vol. 242. 18--35.

Digital Library

[3]

Albert Atserias. 2004. On sufficient conditions for unsatisfiability of random formulas. J. ACM 51, 2, 281--311.

Digital Library

[4]

Albert Atserias and Víctor Dalmau. 2008. A combinatorial characterization of resolution width. J. Comput. Syst. Sci. 74, 3, 323--334.

Digital Library

[5]

Paul Beame and Toniann Pitassi. 1996. Simplified and improved resolution lower bounds. In Proceedings of FOCS. IEEE Computer Society, 274--282.

Digital Library

[6]

Eli Ben-Sasson. 2001. Expansion in proof complexity. Ph.D. dissertation, Hebrew University.

[7]

Eli Ben-Sasson and Nicola Galesi. 2003. Space complexity of random formulae in resolution. Random Struct. Algorithms 23, 1, 92--109.

Digital Library

[8]

Eli Ben-Sasson and Russell Impagliazzo. 2010. Random CNF's are hard for the polynomial calculus. Computat. Complex. 19, 4, 501--519.

Digital Library

[9]

Eli Ben-Sasson and Jakob Nordström. 2011. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Proceedings of ICS, Bernard Chazelle (Ed.), Tsinghua University Press, 401--416.

[10]

Eli Ben-Sasson and Avi Wigderson. 2001. Short proofs are narrow - Resolution made simple. J. ACM 48, 2, 149--169.

Digital Library

[11]

Patrick Bennet, Ilario Bonacina, Nicola Galesi, Tony Huynh, Mike Molloy, and Paul Wollan. 2015. Space proof complexity for random 3-CNFs. arXiv. (2015) http://arxiv.org/abs/1503.01613.

[12]

Archie Blake. 1937. Canonical expressions in Boolean algebra. Ph.D. dissertation, University of Chicago.

[13]

Ilario Bonacina and Nicola Galesi. 2013. Pseudo-partitions, transversality and locality: A combinatorial characterization for the space measure in algebraic proof systems. In Proceedings of ITCS. Robert D. Kleinberg (Ed.), ACM, 455--472.

Digital Library

[14]

Ilario Bonacina, Nicola Galesi, and Neil Thapen. 2014. Total space in resolution. In Proceedings of the 55th Annual IEEE Symposium on Foundations of Computer Science (FOCS). 641--650.

Digital Library

[15]

Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. 2001. Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. Syst. Sci. 62, 2, 267--289.

Digital Library

[16]

Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiri Sgall. 1997. Proof complexity in algebraic systems and bounded depth frege systems with modular counting. Computat. Complex. 6, 3, 256--298.

Digital Library

[17]

Vasek Chvátal and Endre Szemerédi. 1988. Many hard examples for resolution. J. ACM 35, 4, 759--768.

Digital Library

[18]

Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. 1996. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of STOC. Gary L. Miller (Ed.), ACM, 174--183.

Digital Library

[19]

Stephen A. Cook and Robert A. Reckhow. 1979. The relative efficiency of propositional proof systems. J. Symb. Log. 44, 1, 36--50.

[20]

David A. Cox, John Little, and Donal O'Shea. 1997. Ideals, Varieties, and Algorithms - An Introduction to Computational Algebraic Geometry and Commutative Algebra 2nd Ed., Springer. I--XIII, 1--536.

[21]

Juan Luis Esteban, Nicola Galesi, and Jochen Messner. 2004. On the complexity of resolution with bounded conjunctions. Theoret. Comput. Sci. 321, 2--3, 347--370.

Digital Library

[22]

Juan Luis Esteban and Jacobo Torán. 2001. Space bounds for resolution. Inf. Comput. 171, 1, 84--97.

Digital Library

[23]

Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. 2013. Towards an understanding of polynomial calculus: New separations and lower bounds - (Extended Abstract). In Proceedings of ICALP (1), Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg (Eds.), (Lecture Notes in Computer Science) vol. 7965, Springer, 437--448.

Digital Library

[24]

Yuval Filmus, Massimo Lauria, Jakob Nordström, Neil Thapen, and Noga Ron-Zewi. 2012. Space complexity in polynomial calculus. In Proceedings of IEEE Conference on Computational Complexity. IEEE, 334--344.

Digital Library

[25]

Nicola Galesi and Massimo Lauria. 2010a. On the automatizability of polynomial calculus. Theory Comput. Syst. 47, 2, 491--506.

Digital Library

[26]

Nicola Galesi and Massimo Lauria. 2010b. Optimality of size-degree tradeoffs for polynomial calculus. ACM Trans. Comput. Log. 12, 1, 4.

Digital Library

[27]

Russell Impagliazzo, Pavel Pudlák, and Jiri Sgall. 1999. Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Comput. Complex. 8, 2, 127--144.

Digital Library

[28]

Jan Krajíček. 2009. Propositional proof complexity I. Manuscript available at author's webpage.

[29]

Jakob Nordström. 2009. Narrow proofs may be spacious: Separating space and width in resolution. SIAM J. Comput. 39, 1, 59--121.

Digital Library

[30]

Jakob Nordström and Johan Håstad. 2013. Towards an optimal separation of space and length in resolution. Theory Comput. 9, 471--557.

[31]

Pavel Pudlák and Jiří Sgall. 1998. Algebraic models of computation and interpolation for algebraic proof systems. DIMACS Series in Discrete Math. Theoret. Comput. Sci. 39, 279--295.

[32]

Alexander A. Razborov. 1998. Lower bounds for the polynomial calculus. Computat. Complex. 7, 4, 291--324.

Digital Library

[33]

Alexander A. Razborov. 2003. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Manuscript available at author's webpage.

[34]

John Alan Robinson. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12, 1, 23--41.

Digital Library

Cited By

Dantchev SGalesi NGhani AMartin B(2024)Proof Complexity and the Binary Encoding of Combinatorial PrinciplesSIAM Journal on Computing10.1137/20M134784X53:3(764-802)Online publication date: 24-Jun-2024
https://doi.org/10.1137/20M134784X
Dantchev SGhani AMartin B(2020)Sherali-Adams and the Binary Encoding of Combinatorial PrinciplesLATIN 2020: Theoretical Informatics10.1007/978-3-030-61792-9_27(336-347)Online publication date: 3-Dec-2020
https://doi.org/10.1007/978-3-030-61792-9_27
Dantchev SGalesi NMartin BAceto L(2019)Resolution and the binary encoding of combinatorial principlesProceedings of the 34th Computational Complexity Conference10.4230/LIPIcs.CCC.2019.6(1-25)Online publication date: 17-Jul-2019
https://dl.acm.org/doi/10.4230/LIPIcs.CCC.2019.6
Show More Cited By

Index Terms

A Framework for Space Complexity in Algebraic Proof Systems
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation

Recommendations

Space Complexity in Polynomial Calculus
CCC '12: Proceedings of the 2012 IEEE Conference on Computational Complexity (CCC)

During the last decade, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important issue in SAT ...
Algebraic proofs over noncommutative formulas

We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege, yielding a semantic way to define a Cook-Reckhow (...
Automating algebraic proof systems is NP-hard
STOC 2021: Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing

We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula F, it is NP-hard to find a refutation of F in the Nullstellensatz, Polynomial Calculus, or Sherali–Adams proof systems in time polynomial in the size of the shortest such ...

Comments

Information & Contributors

Information

Published In

cover image Journal of the ACM

Journal of the ACM Volume 62, Issue 3

June 2015

263 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/2799630

Editor:
Victor Vianu
University of California, San Diego

Issue’s Table of Contents

Copyright © 2015 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 June 2015

Accepted: 01 November 2014

Revised: 01 March 2014

Received: 01 June 2013

Published in JACM Volume 62, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

John Templeton Foundation under the Project The Limits of Theorem Proving

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
237
Total Downloads

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

Reflects downloads up to 09 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Dantchev SGalesi NGhani AMartin B(2024)Proof Complexity and the Binary Encoding of Combinatorial PrinciplesSIAM Journal on Computing10.1137/20M134784X53:3(764-802)Online publication date: 24-Jun-2024
https://doi.org/10.1137/20M134784X
Dantchev SGhani AMartin B(2020)Sherali-Adams and the Binary Encoding of Combinatorial PrinciplesLATIN 2020: Theoretical Informatics10.1007/978-3-030-61792-9_27(336-347)Online publication date: 3-Dec-2020
https://doi.org/10.1007/978-3-030-61792-9_27
Dantchev SGalesi NMartin BAceto L(2019)Resolution and the binary encoding of combinatorial principlesProceedings of the 34th Computational Complexity Conference10.4230/LIPIcs.CCC.2019.6(1-25)Online publication date: 17-Jul-2019
https://dl.acm.org/doi/10.4230/LIPIcs.CCC.2019.6
Galesi NKolodziejczyk LThapen N(2019)Polynomial Calculus Space and Resolution Width2019 IEEE 60th Annual Symposium on Foundations of Computer Science (FOCS)10.1109/FOCS.2019.00081(1325-1337)Online publication date: Nov-2019
https://doi.org/10.1109/FOCS.2019.00081
Bennett PBonacina IGalesi NHuynh TMolloy MWollan P(2017)Space proof complexity for random 3-CNFsInformation and Computation10.1016/j.ic.2017.06.003255(165-176)Online publication date: Aug-2017
https://doi.org/10.1016/j.ic.2017.06.003
Atserias ALauria MNordström J(2016)Narrow Proofs May Be Maximally LongACM Transactions on Computational Logic10.1145/289843517:3(1-30)Online publication date: 18-May-2016
https://dl.acm.org/doi/10.1145/2898435
Bonacina IGalesi NThapen N(2016)Total Space in ResolutionSIAM Journal on Computing10.1137/15M102326945:5(1894-1909)Online publication date: Jan-2016
https://doi.org/10.1137/15M1023269
Nordström J(2015)On the interplay between proof complexity and SAT solvingACM SIGLOG News10.1145/2815493.28154972:3(19-44)Online publication date: 17-Aug-2015
https://dl.acm.org/doi/10.1145/2815493.2815497

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 Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents