XOR-SAT Phase Transition

A random XOR-SAT instance has N boolean variables and M=α·N XOR clauses (each clause: x_i ⊕ x_j ⊕ x_k = b). For 3-XOR-SAT the satisfiability threshold is exactly α_c = 1 — below it, almost all instances are satisfiable; above, almost all are not. This sharp transition (proved analytically via linear algebra over GF(2)) is the computational phase transition. Gaussian elimination checks satisfiability exactly for XOR-SAT.

Click "Run Experiment" to scan α from 0 to 2