Short $\mathsf{Res}^*(\mathsf{polylog})$ refutations if and only if narrow $\mathsf{Res}$ refutations
Computational Complexity
2013-10-23 v1 Logic in Computer Science
Abstract
In this note we show that any -CNF which can be refuted by a quasi-polynomial refutation has a "narrow" refutation in (i.e., of poly-logarithmic width). We also show the converse implication: a narrow Resolution refutation can be simulated by a short refutation. The author does not claim priority on this result. The technical part of this note bears similarity with the relation between -depth Frege refutations and tree-like -depth Frege refutations outlined in (Kraj\'i\v{c}ek 1994, Journal of Symbolic Logic 59, 73). Part of it had already been specialized to and in (Esteban et al. 2004, Theor. Comput. Sci. 321, 347).
Cite
@article{arxiv.1310.5714,
title = {Short $\mathsf{Res}^*(\mathsf{polylog})$ refutations if and only if narrow $\mathsf{Res}$ refutations},
author = {Massimo Lauria},
journal= {arXiv preprint arXiv:1310.5714},
year = {2013}
}