License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2022.100
URN: urn:nbn:de:0030-drops-164419
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16441/
Go to the corresponding LIPIcs Volume Portal

Papamakarios, Theodoros ; Razborov, Alexander

Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems

pdf-format:
LIPIcs-ICALP-2022-100.pdf (0.7 MB)

Abstract

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, Σ₂ 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.

BibTeX - Entry

@InProceedings{papamakarios_et_al:LIPIcs.ICALP.2022.100,
  author =	{Papamakarios, Theodoros and Razborov, Alexander},
  title =	{{Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{100:1--100:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16441},
  URN =		{urn:nbn:de:0030-drops-164419},
  doi =		{10.4230/LIPIcs.ICALP.2022.100},
  annote =	{Keywords: Proof Complexity, Resolution, Size-Space Trade-offs}
}

Keywords: Proof Complexity, Resolution, Size-Space Trade-offs
Collection: 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)
Issue Date: 2022
Date of publication: 28.06.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI