象棋棋盤上的反棋是和棋

開局：黑方有兩步棋必須找到

棋局中被強制的部分是一條四到五步長的吃子連鎖，主線上有三個分叉。兩個屬於黑方，都決定勝負。一個屬於紅方，並不決定勝負。第四個出現在黑方走出一著輸棋之後，樹的大部分都在它下面。紅方第一著是炮吃馬；兩種選擇互為映象，就稱之為 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。本頁會如實寫明。