BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

Automating Resolution is NP-Hard Atserias, Albert


We show that it is NP-hard to distinguish formulas that have Resolution refutations of almost linear length from formulas that do not even have weakly exponentially long ones. It follows from this that Resolution is not automatable in polynomial time unless P = NP, or in weakly exponential time unless ETH fails. In the talk I will try to explain the process of discovery that led us to the result.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International