Two-Thread Coverage MCTS for SAT and XSAT

We introduce a Monte-Carlo Tree Search solver for SAT and XSAT that pairs WalkSAT-style rollouts with a two-thread symmetry-breaking initialisation: one thread starts from all-true, the other from all-false, bounding each thread's initial Hamming distance to a satisfying assignment by $\lfloor n/2 \rfloor$.

Empirically the solver closes 100/100 SATLIB graph-colouring encodings (flat200-479, sw100) in tens of milliseconds each, 20/20 planted 3-XOR-SAT at $n{=}200$ (median 10~s), 6/6 at $n{=}300$ (median 138~s), and one SAT Competition 2025 instance (this http URL) in 50~ms via the polarity split alone.

On a full 16-round DES key-recovery encoding ($n{=}1976$, $m{=}30072$) it drives the negative-clause count from $\sim 200$ down to 24 (99.9% clauses satisfied) over 7 hours before hitting the S-box plateau.