2026-08-16T22:14:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23708 2025-10-27T10:42:40Z ddc:004 open_access

On the Automatability of Tree-Like k-DNF Resolution Carenini, Gaia de Rezende, Susanna F. Proof Complexity Tree-like k-DNF Resolution Automatability A proof system 𝒫 is said to be automatable in time f(N) if there exists an algorithm that given as input an unsatisfiable formula F outputs a refutation of F in the proof system 𝒫 in time f(N), where N is the size of the smallest 𝒫-refutation of F plus the size of F. Atserias and Bonet (ECCC 2002), observed that tree-like k-DNF resolution is automatable in time N^{c⋅klog N} for a universal constant c. We show that, under the randomized exponential-time hypothesis (rETH), this is tight up to a O(log k)-factor in the exponent, i.e., we prove that tree-like k-DNF resolution, for k at most logarithmic in the number of variables of F, is not automatable in time N^o((k/log k)⋅log N) unless rETH is false. Our proof builds on the non-automatability results for resolution by Atserias and Müller (FOCS 2019), for algebraic proof systems by de Rezende, Göös, Nordström, Pitassi, Robere and Sokolov (STOC 2021), and for tree-like resolution by de Rezende (LAGOS 2021). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Gaia Carenini and Susanna F. de Rezende 2025 Is Part Of LIPIcs, Volume 339, 40th Computational Complexity Conference (CCC 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CCC.2025.14 urn:nbn:de:0030-drops-237081 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.14 eng https://creativecommons.org/licenses/by/4.0/legalcode