Random Walk for 3SAT — Markov Chain Demo

Random Walk for 3SAT

This demo illustrates the random-flip step used in Schöning's randomized 3-SAT algorithm. Select an unsatisfied clause, then flip one of its variables uniformly at random. The diagram tracks how many of the n variables agree with a fixed satisfying assignment. That count alone need not be a Markov chain: the next-step probabilities also depend on the current assignment and selected clause. The fixed solution is shown for analysis; the random-flip rule does not use it.

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 that we don't satisfy, we move towards the fixed solution with probability at least 1/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.