Automating Tree-Like Resolution in Time no(log n) Is ETH-Hard.

We show that tree-like resolution is not automatable in time n ^{o (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 n ^{o (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). [ABSTRACT FROM AUTHOR]