2026-07-26T16:59:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16441 2024-03-06T10:57:29Z ddc:004 open_access

Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems Papamakarios, Theodoros Razborov, Alexander Proof Complexity Resolution Size-Space Trade-offs 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Theodoros Papamakarios and Alexander Razborov 2022 Is Part Of LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2022.100 urn:nbn:de:0030-drops-164419 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.100 eng https://creativecommons.org/licenses/by/4.0/legalcode