Selecting Complementary Pairs of Literals

We present and rigorously analyze a heuristic that searches for a satisfying truth assignment of a given random instance of the 3-SAT problem. We prove that the heuristic asymptotically certainly succeeds in producing a satisfying truth assignment for formulas with clauses to variables ratio (density) of up to 3.52. Thus the experimentally observed threshold of the density where a typical formula's phase changes from asymptotically certainly satisfiable to asymptotically certainly contradictory is rigorously shown to be at least 3.52. The best previous lower bound in the long series of mathematically rigorous approximations by various research groups of the experimental threshold was 3.42. That was the first result where the probabilistic analysis was based on random formulas with a pre-specified, typical number of appearances for each literal. However, in that result, in order to simplify the analysis, the number of appearances of each literal was decoupled from the number of appearances of its negation. In this work, we assume not only that each literal has the typical number of occurrences, but that for each variable both numbers of occurrences of its positive and negated appearances are typical. By standard techniques, our algorithm can be easily modified to run in linear time. Thus not only the satisfiability threshold, but also the threshold (experimental again) where the complexity of searching for satisfying truth assignments jumps from polynomial to exponential is at least 3.52. This should be contrasted with the value 3.9 for the complexity threshold given by theoretical (but not mathematically rigorous) techniques of Statistical Physics.