Experimental results on the crossover point in satisfiability problems

Determining whether a propositional theory is satisfiable is a prototypical example of an NPcomplete 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 a series of experiments to determine the location of the crossover point --- the point at which half the randomly generated propositional theories with a given number of variables and given number of clauses are satisfiable --- and to assess the relationship of the crossover point to the difficulty of determining satisfiability. We have found empirically that, for 3-sat, the number of clauses at the crossover point is a linear function of the number of variables. This result is of theoretical interest since it is not clear why such a linear relationship should exist, but it is also of practical interest since recent experiments [ Mitchell et al. 92; Cheeseman et al. 91 ] indicate that the most comput...