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$.