We consider random 3CNF formulas with n variables and m clauses. It is well known that when m \ge cn (for a sufficiently large constant c), most formulas are not satisfiable. However, it is not known whether such formulas are likely to have polynomial size witnesses that certify that they are not satisfiable. A value of m \simeq n^{3/2} was the forefront of our knowledge in this respect. When m \ge cn^{3/2}, such witnesses are known to exist, based on spectral techniques. When m \le n^{3/2- \in}, it is known that resolution (which is a common approach for refutation) cannot produce witnesses of size smaller than 2^{n^ \in } . Likewise, it is known that certain variants of the spectral techniques do not work in this range.

In the current paper we show that when m \ge cn^{7/5}, almost all 3CNF formulas have polynomial size witnesses for non-satisfiability. We also show that such a witness can be found in time 2^{O\left( {n^{0.2} \log n} \right)} , whenever it exists. Our approach is based on an extension of the known spectral techniques, and involves analyzing a certain fractional packing problem for random 3-uniform hypergraphs.