Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Paper:

TR16-184 | 16th November 2016 22:07

#### On Space and Depth in Resolution

TR16-184
Authors: Alexander Razborov
Publication: 16th November 2016 22:07
Keywords:

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''
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
$s(n)\ll \log n$ and show that no supercritical tradeoff is possible in this