[Proof Complexity] a new preprint

Alexander Razborov razborov at cs.uchicago.edu
Tue Nov 1 22:53:31 CET 2016

Dear Colleagues,

A new paper "On Space and Depth in Resolution" can be downloaded from my
Web page http://people.cs.uchicago.edu/~razborov/research.html

The abstract is enclosed below, and any comments are very welcome.

A. Razborov

We show that the total space in resolution, as well as in any other 
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 
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 
about the same as the question of (non)-existence of ``supercritical''
between the variable space and the proof length. We provide a partial 
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 
$s(n)\ll \log n$ and show that no supercritical tradeoff is possible in this

More information about the Proof-Complexity mailing list