Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

On the automatability of tree-like k-DNF resolution

Carenini, Gaia and de Rezende, Susanna F. LU orcid (2025) 40th Computational Complexity Conference, CCC 2025 In LIPIcs : Leibniz international proceedings in informatics 339.
Abstract

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... (More)

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).

(Less)
Please use this url to cite or link to this publication:
author
and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
keywords
Automatability, Proof complexity, Tree-like k-DNF resolution
host publication
40th Computational Complexity Conference, CCC 2025 : CCC 2025, August 5–8, 2025, Toronto, Canada - CCC 2025, August 5–8, 2025, Toronto, Canada
series title
LIPIcs : Leibniz international proceedings in informatics
editor
Srinivasan, Srikanth
volume
339
pages
21 pages
publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
conference name
40th Computational Complexity Conference, CCC 2025
conference location
Toronto, Canada
conference dates
2025-08-05 - 2025-08-08
external identifiers
  • scopus:105012159035
ISSN
1868-8969
ISBN
9783959773799
DOI
10.4230/LIPIcs.CCC.2025.14
language
English
LU publication?
yes
id
f6155fad-29a6-46ad-8df2-67c14e380b64
date added to LUP
2025-08-12 10:33:48
date last changed
2025-10-14 09:20:47
@inproceedings{f6155fad-29a6-46ad-8df2-67c14e380b64,
  abstract     = {{<p>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 N<sup>c·k</sup> log <sup>N</sup> 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).</p>}},
  author       = {{Carenini, Gaia and de Rezende, Susanna F.}},
  booktitle    = {{40th Computational Complexity Conference, CCC 2025 : CCC 2025, August 5–8, 2025, Toronto, Canada}},
  editor       = {{Srinivasan, Srikanth}},
  isbn         = {{9783959773799}},
  issn         = {{1868-8969}},
  keywords     = {{Automatability; Proof complexity; Tree-like k-DNF resolution}},
  language     = {{eng}},
  month        = {{07}},
  publisher    = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}},
  series       = {{LIPIcs : Leibniz international proceedings in informatics}},
  title        = {{On the automatability of tree-like k-DNF resolution}},
  url          = {{http://dx.doi.org/10.4230/LIPIcs.CCC.2025.14}},
  doi          = {{10.4230/LIPIcs.CCC.2025.14}},
  volume       = {{339}},
  year         = {{2025}},
}