Experimental results on the crossover point in random 3-SAT

Determining whether a propositional theory is satisfiable is a prototypical example of an NP-complete problem. Further, a large number of problems that occur in knowledge-representation, learning, planning, and other areas of AI are essentially satisfiability problems. This paper reports on the most extensive set of experiments to date on the location and nature of the crossover point in satisfiability problems. These experiments generally confirm previous results with two notable exceptions, First, we have found that neither of the functions previously proposed accurately models the location of the crossover point. Second, we have found no evidence of any hard problems in the under-constrained region. In fact the hardest problems found in the under-constrained region were many times easier than the easiest unsatisfiable problems found in the neighborhood of the crossover point. We offer explanations for these apparent contradictions of previous results.