Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Paper:

TR16-057 | 11th April 2016 10:22

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

TR16-057
Authors: Ilario Bonacina
Publication: 12th April 2016 20:49
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)$.