Theory of Computing
-------------------
Title     : Easily refutable subformulas of large random 3CNF formulas
Authors   : Uriel Feige and Eran Ofek
Volume    : 3
Number    : 2
Pages     : 25-43
URL       : http://www.theoryofcomputing.org/articles/v003a002

Abstract
--------
A simple nonconstructive argument shows that most 3-CNF formulas
with  cn  clauses (where  c  is a sufficiently large constant) are
not satisfiable. It is an open question whether there is an
efficient refutation algorithm that for most formulas with  cn
clauses proves that they are not satisfiable.  We present a
polynomial time algorithm that for most 3-CNF formulas with
cn^{3/2}  clauses (where  c  is a sufficiently large constant)
finds a subformula with  \Theta(c^2n)  clauses and then uses
spectral techniques to prove that this subformula is not satisfiable 
(and hence that the original formula is not satisfiable). Previously,
it was only known how to certify efficiently the unsatisfiability of 
random  3-CNF  formulas with at least  polylog(n)n^{3/2}  clauses. 
Our algorithm is simple enough to run in practice. We present some
experimental results.