## Total space in resolution

In this series of talks we cover some results on the space complexity of Resolution and in particular a connection between total space and width. Given a k-CNF formula F, the width is the minimal integer W such that there exists a Resolution refutation of F with clauses of at most W literals. The total space is the minimal size T of a memory used to write down a Resolution refutation of F, where the size of the memory is measured as the total number of literals it can contain. We show that T=\Omega((W-k)^2). This connection between total space and width relies on some basic properties of another, perhaps less known, complexity measure in Resolution: the “asymmetric width”.

This series of talks is based on the following works (Bonacina, 2016; Bonacina, Galesi, & Thapen, 2016; Bonacina, Galesi, & Thapen, 2014).

Talks on this theme were given in:

Feb 06, 2017 **Universidad Politecnica de Catalunya** – *ALBCOM Seminar on Algorithms and Theory of Computation*

Aug 19, 2016 **Fields Institute, Toronto** – *Workshop on Theoretical Foundations of SAT Solving*

Jul 14, 2016 **43rd International Colloquium on Automata, Languages and Programming (ICALP)**

May 30, 2016 **Steklov Institute of Mathematics, St.Petersburg** – *Special Semester on Complexity Theory*

May 19, 2016 **Steklov Institute of Mathematics, St.Petersburg** – *Proof Complexity Workshop*

Oct 20, 2014 **55th Annual Symposium on Foundations of Computer Science (FOCS), Philadelphia**

Oct 16, 2014 **Dagstuhl Seminar 14421** – *Optimal algorithms and proofs*

Jul 13, 2014 **Vienna Summer of Logic, Wien** – *Workshop on proof complexity*

Feb 07, 2014 **KTH Royal Institute of Technology, Stockholm** – Complexity Seminar

## References

*SIAM J. Comput.*,

*45*(5), 1894–1909.

@article{BGT16-siamjcomp, author = {Bonacina, Ilario and Galesi, Nicola and Thapen, Neil}, title = {{Total Space in Resolution}}, journal = {SIAM J. Comput.}, volume = {45}, number = {5}, pages = {1894--1909}, month = jan, year = {2016}, doi = {10.1137/15M1023269} }

*43rd International Colloquium on Automata, Languages, and Programming – ICALP*(Vol. 55, pp. 56:1–56:13).

@inproceedings{Bon16-icalp, author = {Bonacina, Ilario}, title = {{Total Space in Resolution is at Least Width Squared}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming -- ICALP}, pages = {56:1--56:13}, year = {2016}, volume = {55}, doi = {10.4230/LIPIcs.ICALP.2016.56} }

*55th Annu. Symp. Found. Comput. Sci. – FOCS*(Vol. 38, pp. 641–650).

@inproceedings{BGT14-focs, author = {Bonacina, Ilario and Galesi, Nicola and Thapen, Neil}, title = {{Total Space in Resolution}}, booktitle = {55th Annu. Symp. Found. Comput. Sci. -- FOCS}, pages = {641--650}, volume = {38}, year = {2014}, month = oct, doi = {10.1109/FOCS.2014.74} }