Proof-Number Search is a best-first search algorithm with many successful applications, especially in game solving. As large-scale computing clusters become increasingly accessible, parallelization is a natural way to accelerate computation. However, existing parallel versions of Proof-Number Search are known to scale poorly on many CPU cores. Using two parallelized levels and shared information among workers, we present the first massively parallel version of Proof-Number Search that scales efficiently even on a large number of CPUs. We apply our solver, enhanced with Grundy numbers for reducing game trees of impartial games, to the Sprouts game, a case study motivated by the long-standing Sprouts Conjecture. Our algorithm achieves 332.9$\times$ speedup on 1024 cores, significantly improving previous parallelizations and outperforming the state-of-the-art Sprouts solver GLOP by four orders of magnitude in runtime while generating proofs 1,000$\times$ more complex. Despite exponential growth in game tree size, our solver verified the Sprouts Conjecture for 42 new positions, nearly doubling the number of known outcomes.

翻译：证明数搜索是一种最佳优先搜索算法，已在诸多领域特别是游戏求解中取得广泛应用。随着大规模计算集群日益普及，并行化成为加速计算的自然途径。然而，现有证明数搜索的并行版本在大量CPU核心上普遍存在扩展性不足的问题。通过采用双层并行架构及工作节点间的信息共享机制，我们首次实现了能在大规模CPU集群上高效扩展的大规模并行证明数搜索算法。我们将该求解器应用于Sprouts游戏——这一案例研究源于长期存在的Sprouts猜想，并通过引入Grundy数来缩减公平游戏博弈树的规模。实验表明，我们的算法在1024个核心上实现了332.9倍的加速比，显著超越了现有并行方案，其运行时间较当前最优的Sprouts求解器GLOP缩短了四个数量级，同时生成的证明复杂度提升1000倍。尽管博弈树规模呈指数级增长，我们的求解器仍成功验证了Sprouts猜想的42个新局态，使已知结果数量近乎翻倍。