共円(きょうえん)の解答

26-9-26にyuubinnkyokuさんから、二人ゲームとしてサイズ1×1から10×10までの勝敗を解析したという解答が寄せられました。


yuubinnkyokuさんの解答

【対象ルールおよびゲームの定義】

本解析では、2人対戦において、共円または共線が成立した場合は必ず指摘されるという前提を置いています。

よって共円・共線となる4石目を置いた時点で即座に敗北となり、解析においては「自滅手を除外した安全な手のみを着手可能手とし、打てる手がなくなった側を負けとする有限ゲーム」として定式化・解析いたしました。

共円・共線の判定には浮動小数点演算を用いず、4点 (x,y) に対して各行を

[x^2+y^2, x, y, 1]

とする4×4整数行列式が0になるかどうかで厳密に判定しています。

【解析結果】

1×1から10×10までの各盤面について、最適プレイ時の勝者は以下の通りです。

9×9盤では、(0-indexed 座標で)中央の (4,4) に初手を置くと、その後の相手番が負け局面となることを確認しています。

さらに、9×9の81通りの初手を回転・反転対称性で15種類の代表にまとめ、全代表を厳密探索した結果、中央に限らず81点すべての初手が先手勝ちであることを確認しました。

10×10盤についても、100通りの初手を対称性で15種類の代表にまとめた上で厳密探索し、15種類すべてで「その初手を打った先手が負け」となることを確認しました。したがって、10×10では100通りすべての初手が先手負けであり、空盤面は後手必勝です。

【探索手法とAI利用】

本成果は、2026年7月24日にChatGPTへ「共円ゲームは先手有利か後手有利か」という趣旨の質問をしたことが発端です。

その後、「これについてより詳しく研究して」と指示したところ、ChatGPTがC++による探索コードを生成・コンパイル・実行し、まず7×7盤について後手必勝という結果を得ました。さらに対話を通じて探索を8×8、9×9へ拡張し、その後10×10についても解析を進めました。

探索プログラムでは、主に以下の手法を用いています。

これらの探索アルゴリズムや高速化手法を、私自身が事前に設計して実装したものではありません。探索コードの生成・改良・実行・検証のほとんどは、ChatGPTとの対話を通じて行われました。

【9×9中央初手の再現計算】

リポジトリの commit 155a143 のコード(cpp/solvers/kyouen_solver_9.cpp)を手元のPCで再実行しました。

[実行環境]

[再現結果]

115.5秒は、前処理を含むソルバー内部の経過時間です。

共円・共線になる組の数、局面の数、探索した深さは、過去に保存されていた実行記録と完全に一致しました。

【勝敗証明書と独立検証】

AIが出力した探索結果だけに依存しないよう、1×1~9×9については、局面ごとの勝敗などの関係を記録した順位付きDAG証明書を生成させました。

別実装のC++検査器で、証明書中の各局面について、

を再計算し、1×1~9×9の全証明書が検査に合格することを確認しています。

9×9の証明書は、空盤面を根とする13,457,134ノードのDAGです。空盤面から中央 (4,4) を勝ち手として記録し、その後の13,457,133局面の証明DAGに繋げています。

なお、「9×9では81点すべての初手が先手勝ち」という追加結果は、中央以外の14種類のD4初手代表を別途厳密探索して得たものです。公開している9×9の空盤面証明書自体は、中央初手を勝ち手として先手必勝を証明する構成です。

10×10は1×1~9×9とは検証形式が異なります。100種類の初手を対称性から15個の代表にまとめて、最終的に先手勝ちになるか先手負けになるかを分類し、結果をまとめたCSVの構造・対称性・分枝の網羅性などを探索器とは別のRustプログラムで検証しています。

この際、KYOENC4(128-bitで盤面を表現した証明書形式) とRust検査器を実装し、実際の10×10局面について証明DAGを生成・検査しています。ただし、現時点では10×10のすべての初手について空盤面から1本のKYOENC4形式のDAGとして統合するところまでは行っていません。

【Leanによる形式化】

順位付き証明書自体について、

「各ノードの局所的な証明条件が正しく満たされ、順位が厳密に減少するならば、根に記録された勝ち負けの判定は通常プレイの実際の勝敗と一致する」

という一般的な健全性をLeanで形式化・証明しています。

具体的な巨大証明書の読み込みと全ノードの実検査はC++またはRustの検査器が担当し、Leanは証明書方式そのものの一般的な正しさを証明する、という役割分担です。

したがって、具体的な1×1~9×9の巨大証明書をLeanカーネルだけで全件検査しているわけではありません。

【先行研究との比較】

確認できた公開資料では、完全指摘・2人制の共円ゲームについて、3×3~6×6の完全探索結果が報告されており、本解析の3×3~6×6の結果はそれらと一致しています。

また、「共円・共線4点を含まず最大何石置けるか」という極値問題については、少なくとも k(1)~k(9) の値が2018年までに公開されており、これらの値自体は本研究独自の発見ではありません。

2026年9月23日までに確認できた公開資料の範囲では、完全指摘・2人制における7×7、8×8、9×9、10×10盤の勝敗を報告した先行公開例は確認できませんでした。また、これらの盤面について独立検査可能な勝敗証明書を公開した先行例も確認できませんでした。

【公開資料】

ソースコード、探索器、証明書生成器、C++・Rust検査器、Lean形式化コード、検証記録、先行研究調査、および関連する研究データは以下のリポジトリで公開しています。

GitHub:
https://github.com/yuubinnkyoku/kyouen-researches