On the automatability of tree-like k-DNF resolution - Carenini, Gaia; de Rezende, Susanna F. ; 0000-0001-8923-1240 (40th Computational Complexity Conference, CCC 2025, Toronto, Canada, 2025-08-05 - 2025-08-08, 2025)
A proof system P 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 P in time f(N), where N is the size of the smallest P-refutation of F plus the size of F. Atserias and Bonet (ECCC 2002), observed that tree-like k-DNF resolution is automatable in time Nc·k log 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 (Equation presented)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).
Keywords: Automatability; Proof complexity; Tree-like k-DNF resolution