Random 3-SAT Phase Transition Benchmark

What this research found

Uniform random 3-SAT flips abruptly from almost always satisfiable to almost always unsatisfiable as the ratio of clauses to variables rises, and the cost of deciding an instance peaks right at the switch. A complete Davis–Putnam–Logemann–Loveland solver was written from scratch, using no external satisfiability library, and applied to 1,120 random formulae at 50 and 100 variables across 16 constraint densities spanning 3.0 to 6.0. The 50% satisfiability crossover fell at 4.37 for 50 variables and 4.27 for 100, converging on the asymptotic threshold near 4.26, while median solver effort peaked at a density of 4.4 for both sizes.

• The fitted logistic crossover moved from 4.37 at 50 variables to 4.27 at 100, and a model-free linear interpolation gave 4.31 and 4.25. Both estimates converge on the asymptotic threshold of roughly 4.26 established by cavity-method calculations and earlier experiments.
• The transition sharpens as the system grows: fitted logistic steepness rose from 4.10 at 50 variables to 7.29 at 100, close to a two-fold increase from merely doubling the variable count, which is the expected approach to the step function of the infinite-size limit.
• Median running time traced the classic easy–hard–easy profile, cheap when under-constrained, cheap again when over-constrained, and peaking in between at a density of 4.4 for both sizes — 12.69 ms at 50 variables and 254.15 ms at 100.
• Hardware-independent counters peak at exactly the same density, showing the hardness belongs to the search rather than to the timing. Median branching decisions peak at 52 for 50 variables and 428 for 100, and median unit propagations at 408 and 5,620, growth of about 8.2 times and 13.8 times from doubling the variable count.
• All 1,120 instances were decided inside the 5-second per-instance cutoff, so there were zero timeouts and no censored medians. Of those, 511 were satisfiable and 609 unsatisfiable, and every one of the 511 satisfying assignments passed a separately implemented verifier with zero failures.

How it was done

Instances were generated with the standard fixed-clause-length random model — three distinct variables sampled uniformly per clause, each negated with probability one half, duplicate clauses rejected, and every formula run through a structural validator. The solver combined unit propagation, pure-literal elimination, and the Maximum Occurrence in clauses of Minimum size branching heuristic inside a depth-first backtracking search, with a 5-second wall-clock cutoff checked at every node and a three-valued outcome of satisfiable, unsatisfiable, or timeout. The grid swept 16 densities from 3.0 to 6.0 in steps of 0.2, with 50 instances per point at 50 variables and 20 per point at 100, each seeded deterministically from its coordinates so the whole experiment reruns exactly. Satisfiable fractions were fitted to a decreasing logistic sigmoid by non-linear least squares to locate the crossover and its steepness, cross-checked against linear interpolation, and every satisfying assignment was handed to an independently written verifier before being accepted.

Data sources

• 1,120 self-generated uniform random 3-CNF instances: 16 densities with 50 trials each at 50 variables and 20 trials each at 100 variables
• Mitchell, Selman & Levesque, AAAI 1992 — hard and easy distributions of SAT problems
• Cheeseman, Kanefsky & Taylor, IJCAI 1991 — where the really hard problems are
• Mertens, Mézard & Zecchina, Random Structures & Algorithms 28:340 (2006) — cavity-method threshold near 4.267
• Crawford & Auton, Artificial Intelligence 81:31 (1996) — experimental crossover point for random 3-SAT
• Kirkpatrick & Selman, Science 264:1297 (1994) — finite-size scaling of random Boolean satisfiability