TY - GEN
T1 - Automating Tree-Like Resolution in Time n^{o(log n)} Is ETH-Hard
AU - De Rezende, Susanna F.
PY - 2021
Y1 - 2021
N2 - 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).
AB - 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).
U2 - 10.1016/j.procs.2021.11.021
DO - 10.1016/j.procs.2021.11.021
M3 - Paper in conference proceeding
T3 - Procedia Computer Science
SP - 152
EP - 162
BT - Proceedings of the XI Latin and American Algorithms, Graphs and Optimization Symposium.
PB - Elsevier
T2 - XI Latin and American Algorithms, Graphs and Optimization Symposium, LAGOS 2021
Y2 - 17 May 2021 through 21 May 2021
ER -