## Space in algebraic proof systems

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), Lecce** – *Best Italian PhD Thesis in TCS 2016*

May 25, 2015 **Institute of Mathematics, Prague** – *Logic Seminar*

Apr 24, 2015 **Dagstuhl Seminar 15171** – *Theory and Practice of SAT Solving*

Apr 08, 2015 **KTH Royal Institute of Technology** – *Complexity Seminar*

Apr 07, 2015 **KTH Royal Institute of Technology** – *Complexity Seminar*

May 19, 2014 **Aarhus University** – *Complexity Seminar*

Sep 10, 2013 **14th Italian Conference on Theoretical Computer Science (ICTCS), Palermo**

Jun 30, 2013 **CSEDays. Theory 2013, Ekaterinburg** – *Summer School*

Jan 13, 2013 **4th Innovations in Theoretical Computer Science (ITCS), Berkeley**

Sep 27, 2012 **Limits of Theorem Proving, Rome** – *Workshop*

## References

*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 }

*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} }

*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} }

*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} }