A proof system P is called automatizable if there is an algorithm A that, given input a statement phi, runs in time poly(s) and outputs a P-proof of phi of size at most poly(s), where s is the size of the shortest P-proof of phi. It had been a long-standing open problem to determine if resolution is automatizable. In a breakthrough result, Atserias and Muller showed that automating resolution is NP hard. They construct a polynomial time computable transformation A that, on input a CNF phi, outputs an unsatisfiable CNF A(phi) such that:
(i) If phi is satisfiable, A(phi) has polynomial sized resolution refutations
(ii) If phi is not satisfiable, A(phi) does not have any subexponential sized resolution refutation
We shall describe this construction.
