__
TR16-057 | 11th April 2016 10:22
__

#### Total space in Resolution is at least width squared

**Abstract:**
Given an unsatisfiable $k$-CNF formula $\phi$ we consider two complexity measures in Resolution: width and total space. The width is the minimal $W$ such that there exists a Resolution refutation of $\phi$ 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 $\phi$, where the size of the memory is measured as the total number of literals it can contain. We prove that $T=\Omega((W-k)^2)$.