skip to main content
Caltech

TCS+ Talk

Wednesday, February 12, 2020
10:00am to 11:00am
Add to Cal
Annenberg 322
Automating Resolution is NP-Hard
Albert Atserias, Professor, Department of Computer Science, Universitat Politecnica de Catalunya,

Abstract: We show that it is NP-hard to distinguish CNF formulas that have Resolution refutations of almost linear length from CNF 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. The proof of this is simple enough that all its ideas can be explained in a talk. Along the way, I will try to explain the process of discovery that led us to the result. This is joint work with Moritz Müller.

For more information, please contact Bonnie Leung by email at [email protected].