In this talk we cover some results on the space complexity of Resolution and in particular the new recent connection between total space and width in the title. 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.

The talk is based on a paper appeared in ICALP’16.