象棋棋盘上的反棋是和棋

开局：黑方有两步棋必须找到

棋局中被强制的部分是一条四到五步长的吃子连锁，主线上有三个分叉。两个属于黑方，都决定胜负。一个属于红方，并不决定胜负。第四个出现在黑方走出一着输棋之后，树的大部分都在它下面。红方第一着是炮吃马；两种选择互为镜像，就称之为 1. Cxb10。下面的棋盘里，箭头标出的是行棋方的每一种吃法。

主线上有一个判断只依赖搜索。引擎在每着 100,000 节点下判定 2...Cxf1 会输，在一百万节点下也是如此，而证明器在它上面耗尽了预算。如果它确实守得住，黑方就多了一条和棋之路，棋局依然是和棋。

为什么用车吃回会输

证明凭证是一棵树：红方每一着只保留一着，黑方每一着保留所有合法应着。1...Rxb10 的那一份有 1,864 个局面。下面是它的主变。在红方第一着自由着法处，黑方有 42 种合法应着，凭证对每一种都有应对。

一着安静的着法若让对手只剩恰好一种吃法，那就是对手不得不走的着法。红方底线的棋子变成一列队伍，黑方的车被迫吃掉摆到面前的一切，就替红方把这列队伍清空。三十步之后红方一子不剩，赢了。所以黑方唯一的着法是 1...Cxh1。

连锁之后：双方各图什么

左边是 1. Cxb10 Cxh1 2. Rxh1 Rxb10 之后，轮到红方。右边是 2. Cxd10 Kxd10 3. Rxh1 之后，轮到黑方，子力相同，只是将在 d10。引擎从这里出发、在三种预算下的对局，显示了中局在争什么。

你没法主动丢子，只能让对方吃掉。所以每一着都是一次奉送，真正起作用的是对手无法拒绝的奉送：一着安静的着法，让对手只剩恰好一种吃法。

一辆无人守护的车是负担。在它的路径上摆子，它就必须一个个吃掉；用车吃回之所以会输，正是这个原因。所以双方开局都改为送炮。在每着两百万节点的那一局里，3. Cb3 给黑方的炮架到 b1 的马上，随后发生三次吃子，两辆车都成了无人守护的子力。接下来是十四步被迫的吃子，双方子力同步减少。

或者是一场缓慢的兵战。在五百万节点下，双方早期都没找到强制性的奉送，兵卒彼此走近，持续一百步，成对被吃掉，中途还搭进去一个象和一个将。

然后九宫让它成为和棋

要取胜，你必须送掉将、两个士和两个象，而它们谁都离不开家。每一个都只能被走到它跟前的敌方棋子吃掉，而双方都在设法摆脱恰恰是那些棋子。一旦双方都没有了车、马、炮、兵，就再也不可能发生吃子，规则把这判为和棋。

两百万节点那一局在第 35 步到达这里，红方把最后几个可出击的棋子喂给黑方的车，随后在第 44 步重复局面成和。兵战以双方各余一车加九宫棋子收场，这个和棋可以手算验证。黑方的车停在红方任何棋子都够不到的线路上，所以永远不会被迫吃子；任何一方的车都可以随时扔掉；而棋盘上无子可吃时任何着法都合法，于是想等的一方就来回挪士，直到无吃子步数限制终结棋局。

要取胜，你需要对手保留足够的出击力量来吃光你整个九宫，并且被迫动用它。那股力量在对手手里：他们可以把它扔进你无法拒绝的吃子里，可以搁着不动，也可以等。在每一盘引擎对局里，三者之一总在需要时出现；而在随机对弈中，3,000 局里有四分之一成了僵局。

这是和棋的证据，还不是证明。每着五百万节点的搜索在两个存活局面里都没找到胜法。我们没有证明从连锁可能通向的每个局面都存在出路，只是说没有任何搜索找到过没有出路的局面。标题说的就是这个判断和这套几何结构。

能把它改成一个能下的棋吗？

和棋源于一个事实：每方五个棋子只能被对手宁愿扔掉的棋子吃掉。修补方案要么改变这一点，要么改变你必须送掉的东西，要么改变僵局的价值。我们试了四种，走的是同一套裁判、扫描、证明器和自战流程。没有一种做出了像样的棋。

所有僵局都判给子少的一方。这是把 FICS 的困毙规则应用到棋局停下的任何情形，它把冻结的棋盘交给子力更少的一方。随机对弈的未决比例从 26% 降到 4%，且没有偏向（红方 47.9%）。引擎对弈毫无变化：引擎不知道这条规则，所以还是同样的对局，只是判法不同，这对该规则会造就的棋毫无说明力。要正经测试，需要给 Fairy-Stockfish 打补丁，让引擎为子数而下。这是唯一一种既保留棋的辨识度又可能奏效的修补，僵局那个开关已经在内核里，有人想试就能试。

只需送掉将，而不是全部。Codrus 是 1844 年的祖先，目标沿纵线总是够得到，但抛掉可出击棋子的一方仍然永远不会被迫吃掉对方的将。它经由同样的两条开局变化成和，而且更快：28 个终点，25 个负局中有 20 个已被证明，三盘自战和棋。

保留将的王者身份。Losers 是 ICC 的版本，保留将军与将死，被将死或只剩光将的一方获胜。它有胜负，但方向错了：黑方在一百万、两百万和五百万节点下都获胜，把它 16 个终点的连锁回推，结果也是黑方，13 个负局中有 7 个已被证明。将军会暂停吃子义务，而在我们看过的每一条变化里，这个先手都落到后手一方。

放九宫里的棋子出来。这是靠取消禁闭来消除堡垒，而让这些棋子成为象棋棋子的大部分特征也随之消失。我们没有测量它；那是另一张棋盘。

我们是怎么核验的

裁判是一个带有上述规则开关的象棋规则内核。它的着法生成在 209 个局面上与 Fairy-Stockfish 一致，零处分歧。每一盘里都由引擎提议，内核判定、执行并终止棋局，所以一个悄悄按不同规则下棋的引擎会让整轮运行中止。

棋手是 Fairy-Stockfish，通过一个变体配置文件设定。它的评估从未针对这个目标训练过，结果也看得出来：十倍搜索量对一倍搜索量在这里只赢到 10-4 带 6 和，而在普通象棋上是 20-0。这就是开局部分依靠证明的原因。

证明器接收一个局面和一个论断，比如“红方从此处必胜”，然后构建一棵树：胜方每一手保留一着取胜着法，负方每一手保留所有合法应着，一直下到内核判定已经结束的局面。如果这棵树闭合，这个论断就是关于规则的事实，与任何引擎的看法无关。它采用证明数搜索，设有 60 步截断，截断计为进攻方失败，因此证明永远不会依赖它。每个证明都保存为一份证明凭证，另有一个独立的校验器只负责把凭证对照内核重放，别的什么都不做。

扫描：连锁终点谁先走谁赢

内核走遍了开局连锁的每一个分支：605 个局面，166 个终点分布在第 4 到第 18 步之间，其中 72 个在第 14 步，而且其中 130 个终点里至少已有一方的将不在了。撇开镜像，83 个互不相同。引擎从每个终点各下一局，每着 100,000 节点。83 局中有 70 局在再走 14 到 36 步内结束，而胜者就是在终点拥有第一着自由着法的一方，70 局里有 66 局如此。另外 13 局成了僵局，按写下的规则算和棋。

所以在连锁内部，每一次在吃法之间的选择，实际上都是在选择连锁结束时谁先走。以每着一百万节点重跑，十一个判断发生了变化：六个僵局变成胜局，两个胜局耗时更长，三个僵局仍是僵局，没有任何胜局换边。

扫描只找出候选，本身不能定论。它的胜局站住了：在十倍预算下没有一个换边，70 个中有 63 个随后在不依赖引擎的情况下被证明。它的僵局是较弱的证据，因为 13 个里有 6 个在一百万节点下变成了胜局。真正要紧的两个僵局是存活下来的终点，它们在一百万节点下，以及从初始阵型出发、每着最高五百万节点的每一盘对局中，都仍是僵局。

证明

从 70 个分出胜负的终点各自出发，预算为一百万个局面：63 个证明闭合，7 个耗尽预算，没有一个被推翻。证明的中位规模是 19 个局面，是一条单线，防守方的每个应着都是被迫的；最大的是车吃回那一支的 1,864 个局面。校验器 63 个全部通过。分叉表就是这些价值从 100,000 节点扫描沿连锁回推的结果；改用一百万节点扫描评分，在距初始阵型八步以内没有任何价值改变。

每一盘棋，逐步回放

本文依据的每一盘棋都在下面的查看器里：引擎每着一百万、两百万和五百万节点的自战对局；开局连锁 83 个终点各一盘；20 盘阶梯对局，即强引擎从随机开局对阵弱引擎；以及 63 个证明各自的主变。查看器先打开 2M 那盘。列表里的任何一盘都可以选。

我们发布的是什么，而不是一个对局页面

上面的一切都在一个代码库里：规则内核，三段 Fairy-Stockfish 变体配置，开局连锁的全部 166 个终点，每个终点在每种预算下各一盘引擎对局，每一份证明凭证，以及可以直接从该目录打开的对局浏览器。npm run verify 几秒钟内就把每一份凭证对照规则重放一遍，并报告 63、63、20 和 7 项有效；README 里有四条命令，配合一个 Fairy-Stockfish 可执行文件即可复现扫描与证明。

如果你能给出第三条存活的开局、任何一份凭证里的防守，或者从上面的局面出发任何一方的胜法，请去那里提一个 issue。本页会如实写明。