This paper discusses the problem of finding a shortest Resolution proof for a CNF formula of n variables. It is shown that if there is a polynomial-time (superpolynomial-time or subexponential time, respectively) approximation algorithm that finds a nearly shortest proof of length up to S + O(n d ), where S is the length of the shortest proof and d may be any constant, then there is a polynomial-time (superpolynomial-time or subexponential-time, respectively) algorithm that solves the (conventional) satisfiability of CNF formulas. This immediately gives a positive answer to the open problem asking whether finding a shortest Resolution proof is NP-hard.