Random K-SAT, one flip at a time
A random formula of M = αN clauses, each an OR of K random literals, is attacked by the ASAT local search. Watch the unsatisfied clauses die out — or refuse to — and sweep α to see the solvable/unsolvable transition sharpen as N grows.
Based on S. H. Lee, M. Ha, C. Jeon & H. Jeong, “Finite-size scaling in random K-satisfiability problems,” Phys. Rev. E 82, 061109 (2010).
Watch one search
Each cell is a clause. ASAT picks a random unsatisfied clause, tries flipping one of its K variables, and always accepts unless the number of unsatisfied clauses would rise — then it accepts with probability p.
Density of unsatisfied clauses against time, log–log. Dashed line: the paper's decay ρu ∼ t−δ at αc for the selected regime. Time advances by 1/Mu per trial flip, as in the paper.
Solve it by hand
A small instance written out in full. Toggle the variables yourself and watch the clauses light up: a literal is highlighted when it is true, and a clause is satisfied once at least one of its literals is. Or let ASAT take a step to see which move it would make.
Clause size K and noise p come from the controls above. Each variable shows Δ, the change in the number of unsatisfied clauses if you flip it — the quantity ASAT checks before accepting a flip.
Variables
Click to toggle between true and false. Hover to find where a variable appears.
Clauses
Sweep α and watch the transition sharpen
For every size and density, fresh random instances are solved from random starts. The solved fraction Ps drops from 1 to 0 across αc, more abruptly for larger N. Rescaling the axis by N1/ν̄ should make the curves fall on top of each other.
Uses the current K and p from the controls above.
Fraction of solved samples Ps.
Median solving time τH (defined while Ps ≥ ½). Rescaled view divides by Nz̄; the paper's log corrections are left out.
What the paper finds
The authors treat a solution as an absorbing state and the unsatisfied-clause density ρu as the order parameter of a nonequilibrium absorbing phase transition. Below the algorithm's threshold αc the search falls into a solution in a time that stays bounded as N grows; above it, ρu settles to a finite value and the search wanders forever.
The finite-size scaling exponent ν̄ sets how fast the transition window closes, as N−1/ν̄. For 3-SAT they find two values depending on where the algorithm's threshold falls: pure random walk (p = 1) stalls well below the clustering threshold αd ≈ 3.86 and shows mean-field directed-percolation exponents (ν̄ = 2), while optimized ASAT (p ≈ 0.21) reaches beyond αd and shows the same percolation exponents as 2-SAT (ν̄ = 3). The SAT–UNSAT threshold itself sits at αs ≈ 4.267.
| Problem | p | αc | θ | z̄ | δ | ν̄ |
|---|---|---|---|---|---|---|
| 2-SAT | any > 0 | 1.002 | 1.0 | 1.0 | 1.0 | 3.0 |
| 3-SAT (RandomWalkSAT) | 1.00 | 2.6705 | 1.0 | 0.5 | 0.5 | 2.0 |
| 3-SAT (optimized ASAT) | 0.21 | 4.1855 | 1.0 | 1.0 | 1.0 | 3.0 |
Browser-sized systems (N in the hundreds) sit in what the paper calls the regime of serious finite-size effects, so expect the curve crossings to drift from the quoted αc, especially for optimized ASAT, where the paper also needed up to 106 variables and Tmax = 108.