We identify a new class of hard 3-SAT instances, namely a random 3-SAT problems having exactly one solution and as few clauses as possible. It is numerically shown that the running time of complete methods as well as of local search algorithms for such problems is larger than for random instances around the phase transition point. We therefore provide instances with an exponential complexity in the so-called easy'' region, below the critical value of m n. This puts a new light on the connection between the phase transition phenomenon and NP-completeness.
 Abstract 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. 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 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 [ 92; 91] indicate that the most computationally difficult problems tend to be found near the crossover point. We have also found that for random 3-SAT problems below the crossover point, the average time complexity of satisfiability problems seems empirically to grow linearly with problem size. At and above the crossover point the complexity seems to grow exponentially, but the rate of growth seems to be greatest near the crossover point.