Automating Resolution is NP-Hard

Albert Atserias, Moritz Müller

We show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NP-hard. In the parlance of proof complexity, Resolution is n…