  Let c>0 be a constant, and $\Phi$ be a random Horn formula with n variables
and $m=c\cdot 2^{n}$ clauses, chosen uniformly at random (with repetition) from
the set of all nonempty Horn clauses in the given variables. By analyzing \PUR,
a natural implementation of positive unit resolution, we show that
$\lim_{n\goesto \infty} \PR ({$\Phi$ is satisfiable})= 1-F(e^{-c})$, where
$F(x)=(1-x)(1-x^2)(1-x^4)(1-x^8)... $. Our method also yields as a byproduct an
average-case analysis of this algorithm.
