I Built a SAT Solver Inspired by Quantum Field Theory and It Works (sethuiyer.github.io)

A new paper presents "Casimir‑SAT," a radical SAT solver that recasts Boolean assignments as microstates in a continuous energy landscape and borrows the Casimir effect to drive coagulation of nearly‑satisfying regions into solutions. Clauses are relaxed to a differentiable fractional satisfaction s_c(x)=1−∏(1−x_ℓ) and the global energy E(x)=∑(1−s_c(x))^2 is minimized by Langevin dynamics with annealing. Crucially, satisfied regions naturally "freeze" (zero gradient), while a distance‑weighted Casimir potential V_C(i,j)=−exp(−d_ij/ξ)|∇_iE||∇_jE| introduces short‑range attractive forces that pull low‑energy blobs together. The algorithm alternates continuous dynamics, sigmoidal projection to [0,1], spectral identification of clusters via a weighted Laplacian/Fiedler vector, contraction of frozen blobs, and focused updates on domain walls; learned gradient‑based clauses play the role of CDCL without explicit backtracking. Technically this yields a hybrid physics/algorithmic pipeline: vectorizable gradient and energy computation (GPU friendly), spectral clustering to detect coagulated structure, and a fall‑back to conventional solvers once walls shrink below ~20 variables. For random 3‑SAT the authors prove expected polynomial-time convergence for clause density α<3.86 and show an exponential spectral gap decay above that threshold—giving an automatic hardness indicator. Tradeoffs are explicit: spectral clustering dominates cost (expected O(n^3 log n) below the threshold), and the method may fail to converge in fragmented phases, but it offers a novel, interpretable paradigm linking phase transitions, nonlocal forces, and SAT solving that could inspire new heuristics and hardness diagnostics.