Automating Tree -Like Resolution in Time n(o) ((logn)) 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 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 GOOs, Nordstrom, Pitassi, Robere and Sokolov (STOC 2021), which presents a simplification of the recent breakthrough of Atserias and Mailer (FOCS 2019). (C) 2021 The Authors. Published by Elsevier B.V.