Logic seminar
Automating Algebraic Proof Systems is NP-Hard
Susana F. de Rezende
IM CAS
Monday, 11. May 2020 - 13:30 to 15:00
https://us02web.zoom.us/j/472648284 - meeting ID: 472 648 284
Recently, Atserias and Müller (FOCS 2019) established that it is NP-hard to find a resolution refutation of an unsatisfiable formula in time polynomial in the size of the shortest such refutation. In this talk, I will present a simplified proof of this result and explain how it can be extended to hold also for Nullstellensatz, Polynomial Calculus, and Sherali–Adams. This is based on joint work with Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere and Dmitry Sokolov.