AI 中文总结
该研究针对SAT和XSAT问题，提出双线程覆盖蒙特卡洛树搜索求解器，结合WalkSAT式展开与双线程对称破缺初始化，在解决多种编码问题上表现出色，如快速解决SATLIB图着色编码、植入的3 - XOR - SAT及SAT竞赛实例，还能有效处理DES密钥恢复编码。
AI 中文摘要
我们介绍了一种用于SAT和XSAT的蒙特卡洛树搜索求解器，它将类似WalkSAT的展开与双线程对称破缺初始化相结合：一个线程从全真开始，另一个从全假开始，将每个线程到满足赋值的初始汉明距离限制为⌊n/2⌋。实验上，该求解器能在几十毫秒内解决100/100个SATLIB图着色编码（flat200 - 479，sw100），在n = 200时能解决20/20个植入的3 - XOR - SAT（中位数10秒），n = 300时能解决6/6个（中位数138秒），还能在50毫秒内通过极性拆分解决一个2025年SAT竞赛实例。在完整的16轮DES密钥恢复编码（n = 1976，m = 30072）上，它能在7小时内将负子句数从约200降至24（99.9%的子句得到满足），然后达到S盒平稳期。
英文摘要
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.
