__
TR16-184 | 16th November 2016 22:07
__

#### On Space and Depth in Resolution

**Abstract:**
We show that the total space in resolution, as well as in any other reasonable

proof system, is equal (up to a polynomial and $(\log n)^{O(1)}$ factors) to

the minimum refutation depth. In particular, all these variants of total space

are equivalent in this sense. The same conclusion holds for variable

space as long as we penalize for excessively (that is, super-exponential) long

proofs, which makes the question about equivalence of variable space and depth

about the same as the question of (non)-existence of ``supercritical''

tradeoffs

between the variable space and the proof length. We provide a partial negative

answer to this question: for all $s(n)\leq n^{1/2}$ there exist CNF

contradictions $\tau_n$ that possess refutations with variable space $s(n)$

but such that every refutation of $\tau_n$ with variable space $o(s^2)$ must

have double exponential length $2^{2^{\Omega(s)}}$. We also include a much

weaker tradeoff result between variable space and depth in the opposite range

$s(n)\ll \log n$ and show that no supercritical tradeoff is possible in this

range.