The probabilistic analysis of a greedy satisfiability algorithm

Consider the following simple, greedy Davis-Putnam algorithm applied to a random 3-CNF formula of constant density c: Arbitrarily set to TRUE a literal that appears in as many clauses as possible, irrespective of their size (and irrespective of the number of occurrences of the negation of the literal). Reduce the formula. If any unit clauses appear, then satisfy their literals arbitrarily, reducing the formula accordingly, until no unit clause remains. Repeat. We prove that for c < 3.42 a slight modification of this algorithm computes a satisfying truth assignment with probability asymptotically bounded away from zero. Previously, algorithms of increasing sophistication were shown to succeed for c < 3.26. Preliminary experiments we performed suggest that c similar or equal to 3.6 is feasible running algorithms like the above, which take into account not only the number of occurrences of a literal but also the number of occurrences of its negation, irrespectively of clause-size information.