Two-Thread Coverage MCTS for SAT and XSAT

Marcel Crasmaru

Two-Thread Coverage MCTS for SAT and XSAT

Optimization and Control 2026-07-17 v1

Authors: Marcel Crasmaru

Abstract

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 (Break-triple-04-06.xml.cnf) 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.

Cite

@article{arxiv.2607.15834,
  title  = {Two-Thread Coverage MCTS for SAT and XSAT},
  author = {Marcel Crasmaru},
  journal= {arXiv preprint arXiv:2607.15834},
  year   = {2026}
}