Abstract. It is known that random k-SAT formulas with at least
(2^k*ln2)*n random clauses are unsatisfiable with high probability. This
result is simply obtained by bounding the expected number of satisfy-
ing assignments of a random k-SAT instance by an expression tending
to 0 when n, the number of variables tends to infinity. This argument
does not give us an efficient algorithm certifying the unsatisfiability of a
given random instance. For even k it is known that random k-SAT in-
stances with at least Poly(logn)*n^(k/2) clauses can be efficiently certified
as unsatisfiable. For k = 3 we need at least n^((3/2)+epsilon) random clauses.
In case of even k we improve the aforementioned results in two ways.
There exists a constant C such that 4-SAT instances with at least C*n^2
clauses can be efficiently certified as unsatisfiable. Moreover, we give
a satisfiability algorithm which runs in expected polynomial time over
all k-SAT instances with C*n^(k/2) clauses. Our proofs are based on the
direct application of known approximation algorithms on the one hand,
and on a recent estimate of the theta-function for random graphs with a
linear number of edges, on the other hand.