We consider logical proof systems from the point of view of their space complexity, in particular we focus on the following two: Resolution (RES), a well studied proof system that is at the core of state-of-the-art algorithms to solve SAT instances; Polynomial Calculus (PC), a proof system that uses polynomials to refute contradictions. Informally speaking, the space of a proof measures the size of an auxiliary memory that a verifier needs to check the correctness of the proof. For Polynomial Calculus the space measure counts the number of distinct monomials to be kept in memory (monomial space). For Resolution the measure refers to the number of clauses to be kept in memory (clause space) or to the total number of symbols (total space). We introduce abstract frameworks to prove monomial space lower bounds in PC and total space lower bound in RES. We then exemplify such frameworks proving new (asymptotically) optimal lower bounds both for monomial space and total space. We prove that every Polynomial Calculus refutation of a random k-CNF F, for k > 2, in n variables requires, with high probability, \Omega(n) distinct monomials to be kept simultaneously in memory.

This series of talks is based on the following works (Bonacina, 2015; Bonacina & Galesi, 2013; Bonacina & Galesi, 2015; Bennett et al., 2015).

Talks on this theme were given in:

Sep 13, 2016 17th Italian Conference on Theoretical Computer Science (ICTCS), LecceBest Italian PhD Thesis in TCS 2016
May 25, 2015 Institute of Mathematics, PragueLogic Seminar
Apr 24, 2015 Dagstuhl Seminar 15171Theory and Practice of SAT Solving
Apr 08, 2015 KTH Royal Institute of TechnologyComplexity Seminar
Apr 07, 2015 KTH Royal Institute of TechnologyComplexity Seminar
May 19, 2014 Aarhus UniversityComplexity Seminar
Sep 10, 2013 14th Italian Conference on Theoretical Computer Science (ICTCS), Palermo
Jun 30, 2013 CSEDays. Theory 2013, EkaterinburgSummer School
Jan 13, 2013 4th Innovations in Theoretical Computer Science (ITCS), Berkeley
Sep 27, 2012 Limits of Theorem Proving, RomeWorkshop

References

Bonacina, I. (2015, December). Space in weak propositional proof systems (PhD thesis). Sapienza University of Rome.
@phdthesis{Bonacina-phdthesis,
  author = {Bonacina, Ilario},
  title = {Space in weak propositional proof systems},
  school = {Sapienza University of Rome},
  year = {2015},
  month = dec
}

Bonacina, I., & Galesi, N. (2015). A Framework for Space Complexity in Algebraic Proof Systems. J. ACM, 62(3), 1–20.
@article{BG15-jacm,
  author = {Bonacina, Ilario and Galesi, Nicola},
  title = {{A Framework for Space Complexity in Algebraic Proof Systems}},
  journal = {J. ACM},
  volume = {62},
  number = {3},
  pages = {1--20},
  year = {2015},
  month = jun,
  doi = {10.1145/2699438}
}

Bennett, P., Bonacina, I., Galesi, N., Huynh, T., Molloy, M., & Wollan, P. (2015). Space proof complexity for random 3-CNFs. CoRR, abs/1503.01613.
@article{BBGHMW15-preprint,
  author = {Bennett, Patrick and Bonacina, Ilario and Galesi, Nicola and Huynh, Tony and Molloy, Mike and Wollan, Paul},
  title = {Space proof complexity for random 3-CNFs},
  journal = {CoRR},
  volume = {abs/1503.01613},
  year = {2015}
}

Bonacina, I., & Galesi, N. (2013). Pseudo-partitions, transversality and locality: A Combinatorial Characterization for the Space Measure in Algebraic Proof Systems. In 4th Conf. Innov. Theor. Comput. Sci. – ITCS (pp. 455–472).
@inproceedings{BG13-itcs,
  author = {Bonacina, Ilario and Galesi, Nicola},
  title = {{Pseudo-partitions, transversality and locality: A Combinatorial Characterization for the Space Measure in Algebraic Proof Systems}},
  booktitle = {4th Conf. Innov. Theor. Comput. Sci. -- ITCS},
  pages = {455--472},
  year = {2013},
  doi = {10.1145/2422436.2422486}
}