The probabilistic analysis of a greedy satisfiability algorithm