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 CatalunyaALBCOM Seminar on Algorithms and Theory of Computation
Aug 19, 2016 Fields Institute, TorontoWorkshop 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.PetersburgSpecial Semester on Complexity Theory
May 19, 2016 Steklov Institute of Mathematics, St.PetersburgProof Complexity Workshop
Oct 20, 2014 55th Annual Symposium on Foundations of Computer Science (FOCS), Philadelphia
Oct 16, 2014 Dagstuhl Seminar 14421Optimal algorithms and proofs
Jul 13, 2014 Vienna Summer of Logic, WienWorkshop on proof complexity
Feb 07, 2014 KTH Royal Institute of Technology, Stockholm – Complexity Seminar

References

Bonacina, I., Galesi, N., & Thapen, N. (2016). Total Space in Resolution. 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}
}

Bonacina, I. (2016). Total Space in Resolution is at Least Width Squared. In 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}
}

Bonacina, I., Galesi, N., & Thapen, N. (2014). Total Space in Resolution. In 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}
}