Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR21-074 | 3rd June 2021 19:19

Space characterizations of complexity measures and size-space trade-offs in propositional proof systems


Authors: Theodoros Papamakarios, Alexander Razborov
Publication: 3rd June 2021 19:20
Downloads: 485


We identify two new big clusters of proof complexity measures equivalent up to
polynomial and $\log n$ factors. The first cluster contains, among others,
the logarithm of tree-like resolution size, regularized (that is, multiplied
by the logarithm of proof length) clause and monomial space, and clause
space, both ordinary and regularized, in regular and tree-like resolution. As
a consequence, separating clause or monomial space from the (logarithm of)
tree-like resolution size is the same as showing a strong trade-off between
clause or monomial space and proof length, and is the same as showing a
super-critical trade-off between clause space and depth. The second cluster
contains width, $\Sigma_2$ space (a generalization of clause
space to depth 2 Frege systems), both ordinary and regularized, as well as
the logarithm of tree-like size in the system $R(\log)$. As an application of some of
these simulations, we improve a known size-space trade-off for polynomial calculus with resolution. In
terms of lower bounds, we show a quadratic lower bound on tree-like
resolution size for formulas refutable in clause space $4$. We introduce on
our way yet another proof complexity measure intermediate between depth and
the logarithm of tree-like size that might be of independent interest.

ISSN 1433-8092 | Imprint