在位置超级劫下求解围棋：可靠的证明迁移与新的棋盘价值

位置超级劫（PSK）禁止重新形成任何此前出现过的完整棋盘局面。它是书面中国规则的一部分，也是计算机围棋所采用规则的一部分。然而，几乎所有已求解的围棋棋盘都是在更简单的基本劫规则下计算的。PSK使求解变得困难：合法性取决于完整对局历史，而这会破坏使求解变得可行的三种工具，即转置表（图-历史交互问题）、静态死活判断和安全着法剪枝。我们提出 Sanko，一种并行的深度优先证明数求解器，能够在保证正确性的前提下恢复这三种工具。其核心是一条开销很低的证明迁移定理：除非证明获胜方必须创造的某个棋盘局面已经出现过，否则已存储的证明在新路径上仍然有效。Sanko 用六个线程在16分钟内证明了5x5围棋，此前的最佳成绩在六个进程下需要5.25小时；在一台192线程机器上，它只需约1分30秒。它还首次确定了另外23个棋盘在PSK下的价值，其中11个在任何规则下都尚未求解。超级劫会改变博弈论价值：4x7在基本劫下是全盘胜，但在PSK下价值仅为12分；我们还精确指出了此前发表的最优变化在哪一步失效。不同于早期对空棋盘围棋的求解，我们发布了求解器源代码，以及支撑这些价值和测量结果的每次运行的命令行和结果，因此所有报告的价值都可以复现。