Experimental results on the crossover point in satisfiability problems

TLDR

Satisfiability of propositional theories is a prototypical NP‑complete problem, and many AI domains such as knowledge representation, learning, and planning reduce to SAT. The study aims to locate the SAT crossover point and examine its relation to problem difficulty. The authors conduct experiments on randomly generated propositional theories varying variables and clauses to identify the crossover point and analyze its impact on satisfiability difficulty. For 3‑SAT, the crossover point scales linearly with the number of variables; problems near this point are hardest, with sub‑crossover instances growing linearly in time and super‑crossover instances growing exponentially, peaking at the crossover.

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 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 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.