The  importance of  studying the  complexity of  (propositional) proof
systems  comes from  its  close relationship  with long-standing  open
problems in  Complexity Theory such  as NP =?  Co-NP.   The complexity
measure  related to  the classical  notion of  time is  the size  of a
proof, ie the number of lines used in the proof.

Recently  Esteban  and  Toran   suggested  a  measure  for  the  space
complexity  of refusing  an unsatisfiable  formula in  a  proof system
called resolution.

Although several results are, by now, known on the space complexity of
various  classes of  formulae, a  quantitative analysis  of  the space
needed  to prove  the  unsatisfiability of  random formulae  remained,
until recently, somewhat elusive.

As an initial step towards the  solution of this problem, we point out
that  a  combination  of  a  variant  of  the  classical  Davis-Putnam
algorithm  and a linear  time algorithm  for 2-SAT  outputs resolution
refutations  of  any unsatisfiable  random  formula  within the  space
bounds stated in the following Theorem.

Theorem 1.   For each $k>1$ there  are constants $c_1$  and $c_2$ such
that almost all unsatisfiable $k$-CNF formula $F$ on $n$ variables and
$m = \Delta n$ clauses with $\Delta  > c_1$ can be refused in space $k
c_2 n/\Delta^(1/(k-2))$.

REMARKS: (1) Tight upper-bounds on the probability that a random 2-CNF
formula  is  satisfiable are  instrumental  to  the  proof of  Theorem
1. Therefore this Theorem represents  a nice application of results on
the sharp phase-transition phenomenon of random 2-SAT.  (2) For $k=3$,
$c_1=20$ and $c_2=1.1$, but no attempt has been made to optimise these
values. (3) Theorem  1 pairs up with the  lower bounds proved recently
by Ben-Sasson and  Galesi, showing the optimality of  their result for
sufficiently large values of $c_1$.