English

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 kk-CNF which can be refuted by a quasi-polynomial Res(polylog)\mathsf{Res}^*(\mathsf{polylog}) refutation has a "narrow" refutation in Res\mathsf{Res} (i.e., of poly-logarithmic width). We also show the converse implication: a narrow Resolution refutation can be simulated by a short Res(polylog)\mathsf{Res}^*(\mathsf{polylog}) refutation. The author does not claim priority on this result. The technical part of this note bears similarity with the relation between dd-depth Frege refutations and tree-like d+1d+1-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 Res\mathsf{Res} and Res(k)\mathsf{Res}(k) 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}
}
R2 v1 2026-06-22T01:51:18.964Z