Given a satisfiability instance in conjuntive normalform beyond
the satisfiability threshold we know on probabilistic grounds 
that this instance should be unsatisfiable.  The proof of this 
is by a standard first-moment argument.
 
We ask for efficient algorithms certifying the unsatisfiability
of such a formula. Previous work has shown that for even
clause size k formulas with poly(log n) n^{k/2} many k-clauses
can  be certified unsatisfiable in this sense.  We show how 
classical approximation algorithms can be applied to improve on
this result.  They allow to remove the poly(log n)-factor 
leaving us with n^{k/2} many random clauses such that an 
efficient certification is possible.