Random Walk for 3SAT — Markov Chain Demo

Random Walk for 3SAT

This demo shows Schöning's algorithm that can solve 3-SAT in expected time O(1.34ⁿ). We will show O(1.74ⁿ) in the class. At each step: pick a uniformly random variable from an arbitrary unsatisfied clause. 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 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.