The SAT Phase Transition

We describe a detailed experimental investigation of the phase transition for several different classes of randomly generated satisfiability problems. We observe a remarkable consistency of features in the phase transition despite the presence in some of the problem classesof clausesof mixed lengths. For instance, each of the problem classes considered has a sharp transition from satisfiable to unsatisfiable problems at a critical value. In addition, there is a common easy-hard-easy pattern in the median difficulty of the problems, with the hardest problems being associated with the phase transition. However, the difficulty of problems of mixed clause lengths is much more variable than that of fixed clause length. Indeed, whilst the median difficulty of random problems of mixed clause lengths can be orders of magnitude easier than that of equivalently sized problems of fixed clause length, the hardest problems of mixed clause lengths can be orders of magnitude harder than the hardest e...

• Type: Conference
• Year: 1994
• Where: ECAI
• Authors: Ian P. Gent, Toby Walsh
• Keywords: Artificial Intelligence, Clause Length, ECAI 1994, Mixed Clause Lengths, Phase Transition