Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Automating Tree-Like Resolution in Time n^{o(log n)} Is ETH-Hard

De Rezende, Susanna F. LU orcid (2021) XI Latin and American Algorithms, Graphs and Optimization Symposium, LAGOS 2021 In Procedia Computer Science 195. p.152-162
Abstract
We show that tree-like resolution is not automatable in time no(log n) unless ETH is false. This implies that, under ETH, the algorithm given by Beame and Pitassi (FOCS 1996) that automates tree-like resolution in time no(log n) is optimal. We also provide a simpler proof of the result of Alekhnovich and Razborov (FOCS 2001) that unless the fixed parameter hierarchy collapses, tree-like resolution is not automatable in polynomial time. The proof of our results builds on a joint work with Göös, Nordström, Pitassi, Robere and Sokolov (STOC 2021), which presents a simplification of the recent breakthrough of Atserias and Müller (FOCS 2019).
Please use this url to cite or link to this publication:
author
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
Proceedings of the XI Latin and American Algorithms, Graphs and Optimization Symposium.
series title
Procedia Computer Science
volume
195
pages
152 - 162
publisher
Elsevier
conference name
XI Latin and American Algorithms, Graphs and Optimization Symposium, LAGOS 2021
conference location
Sao Paulo, Brazil
conference dates
2021-05-17 - 2021-05-21
external identifiers
  • scopus:85122938721
ISSN
1877-0509
DOI
10.1016/j.procs.2021.11.021
language
English
LU publication?
no
id
4015cac1-a1ad-40aa-9e29-055c9f2ddada
date added to LUP
2022-01-07 23:04:25
date last changed
2025-10-14 11:30:40
@inproceedings{4015cac1-a1ad-40aa-9e29-055c9f2ddada,
  abstract     = {{We show that tree-like resolution is not automatable in time no(log n) unless ETH is false. This implies that, under ETH, the algorithm given by Beame and Pitassi (FOCS 1996) that automates tree-like resolution in time no(log n) is optimal. We also provide a simpler proof of the result of Alekhnovich and Razborov (FOCS 2001) that unless the fixed parameter hierarchy collapses, tree-like resolution is not automatable in polynomial time. The proof of our results builds on a joint work with Göös, Nordström, Pitassi, Robere and Sokolov (STOC 2021), which presents a simplification of the recent breakthrough of Atserias and Müller (FOCS 2019).}},
  author       = {{De Rezende, Susanna F.}},
  booktitle    = {{Proceedings of the XI Latin and American Algorithms, Graphs and Optimization Symposium.}},
  issn         = {{1877-0509}},
  language     = {{eng}},
  pages        = {{152--162}},
  publisher    = {{Elsevier}},
  series       = {{Procedia Computer Science}},
  title        = {{Automating Tree-Like Resolution in Time n^{o(log n)} Is ETH-Hard}},
  url          = {{http://dx.doi.org/10.1016/j.procs.2021.11.021}},
  doi          = {{10.1016/j.procs.2021.11.021}},
  volume       = {{195}},
  year         = {{2021}},
}