{"id":"arxiv/2607.15834","url":"https://arxiv.org/abs/2607.15834","tags":["math.OC"],"score":0,"title":"Two-Thread Coverage MCTS for SAT and XSAT","domain":"math.OC","source":"arxiv","authors":["Marcel Crasmaru"],"reviews":0,"subject":"math.OC","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-17","reactions":{}}