slideshow 3

Logic seminar

Automating tree-like resolution in time n^o(log n/ log log n) is ETH-hard

Susanna F. de Rezende
IM CAS

 

Monday, 30. November 2020 - 15:30 to 17:00
Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284
It is known that tree-like resolution is automatable in time n^O(log n). In this talk we will show that under ETH tree-like resolution is not automatable in time n^o(log n/ log log n). We will also provide an alternative, arguably simpler proof of the result of Alekhnovich and Razborov (SIAM J. Comput. 2008) that unless the fixed parameter hierarchy collapses, tree-like resolution is not automatable in polynomial time. The proof builds on a joint work with Mika Göös, Jakob Nordström, Toni Pitassi, Robert Robere and Dmitry Sokolov (ECCC 2020), which presents a simplification of the breakthrough result of Atserias and Müller (JACM 2020).