What does "refuting random 3CNF" formulas mean?
A random 3CNF with $n$ variables and $m$ clauses is obtained by picking $m$ clauses uniformly at random among the $8\binom{n}{3}$ different clauses. It is known that there exists a constant $C$ such that when $m = Cn$, a random 3CNF is unsatisfiable with high probability; it is strongly suspected that there exists a best such constant $C$, which is known experimentally to be about $4.2$.

It seems, therefore, that if I give you a random 3CNF with $n$ variables and $100n$ clauses, it should be easy to prove that it's unsatisfiable (unless you're very unlucky). However, the best such algorithm, due to Feige and Ofek, only works for $m = \Omega(n^{1.5})$. The best non-deterministic algorithm, due to Feige, Kim and Ofek, only works for $m = \Omega(n^{1.4})$.

One can state many conjectures of the form "refuting random 3CNF formulas is hard". The weakest would state that for every $C &gt; 0$, there is no polynomial time algorithm that, given a formula, answers either unsatisfiable or don't know, and (i) answers unsatisfiable with high probability when given a random 3CNF with $n$ variables and $Cn$ clauses, (ii) answers unsatisfiable only for unsatisfiable formulas.

Stronger conjectures would work for $n^{1+\epsilon}$ clauses for some $\epsilon &gt; 0$, and for non-deterministic polynomial time algorithms.