Random Walk for 3SAT — Markov Chain Demo

Random Walk for 3SAT

At each step: pick a uniformly random unsatisfied clause, then flip a uniformly random variable from it. Track the Hamming agreement with a fixed satisfying assignment, visualized as a 1-D Markov chain on states 0..n.

Speed

DIMACS CNF (≤ 20 variables)

Fixed satisfying assignment (0/1 or ±1, space-separated). Leave empty to auto-solve.

Clauses

Agreement with fixed assignment nodes 0..n

After selecting a clause with k literals matching the fixed assignment, the step goes “towards” the fixed solution with probability (3−k)/3 and “away” with probability k/3.

Context. This walk is the core move used in local-search SAT solvers (e.g. WalkSAT) and also appears in theoretical algorithms. A classic example is Schöning’s algorithm for 3-SAT. Learn more: Schöning’s algorithm · Boolean satisfiability problem.