Eran Ofek, Uriel Feige

Let $\phi$ be a 3CNF formula with n variables and m clauses. A

simple nonconstructive argument shows that when m is

sufficiently large compared to n, most 3CNF formulas are not

satisfiable. It is an open question whether there is an efficient

refutation algorithm that for most such formulas proves ...
more >>>