【Tokyo Doves】後退解析により勝敗確定局面を全列挙する（中断）

お久しぶりです。前回宣言したように、今回は後退解析についてお話ししたいと思います。

解析の進捗
後退解析とは？
局面の分類
局面の分類の全列挙
- Lose から Win を列挙する方法
- Win から Lose を列挙する方法
まとめ

解析の進捗

本題に入る前に、現在の最新の解析状況を表にしておきます。縦軸が局面のステータス、横軸が盤上のハトの数です。表に記入された数は局面数で、プレイヤーの入れ替えや盤の反転・回転・平行移動で一致するものは同一視しています。表の意味は本文を読めばわかります（そう信じています）。

羽数→	3	4	5	6	7	8	9	10	11	12
Lose2	0	0	0	14,310	842,656	21,923,937	248,790,189	1,203,251,971	2,188,848,474	1,115,844,415
Win3	0	0	1,092	286,875	9,258,860	140,471,598	982,711,798	2,994,063,684	3,566,747,816	1,223,384,244
Lose4	0	0	0	14,780	1,159,498	27,325,271	271,375,132	1,142,235,376	1,936,412,932	1,000,573,577
Win5	0	0	3,686	426,101	12,334,687	151,119,509	867,610,689	2,300,144,531	2,561,639,690	886,877,764
Lose6	0	0	0	19,759	1,429,340	29,530,382	246,289,559	886,331,315	1,293,617,107	570,249,480
Win7	0	0	11,460	656,453	14,970,130	155,645,753	764,664,428	1,769,671,531	1,765,494,268	547,295,394
Lose8	0	0	517	46,074	2,167,307	38,248,876	276,966,948	856,583,377	1,070,971,393	409,327,184
Win9	0	245	24,123	1,045,355	19,661,548	175,976,101	764,770,534	1,595,727,389	1,459,223,340	430,422,153
Lose10	0	0	1,424	96,946	3,322,086	47,262,577	293,270,795	811,354,419	930,065,494	324,044,126
Win11	0	684	40,150	1,432,515	22,786,960	181,855,095	729,290,251	1,430,798,207	1,242,095,064	343,567,756
Lose12	0	16	3,390	179,450	4,640,840	54,236,180	296,903,795	762,794,640	832,529,837	274,675,325
Win13	8	1,035	53,330	1,670,839	24,201,201	179,707,675	684,561,345	1,292,930,115	1,087,502,116	293,943,361
Lose14	0	89	5,834	272,705	5,835,522	59,478,800	300,995,897	734,697,610	769,200,808	247,200,282
Win15	5	1,048	59,496	1,756,076	24,238,602	174,048,505	648,881,050	1,203,754,695	986,722,317	260,318,893
Lose16	0	104	7,702	336,047	6,629,846	63,636,151	307,437,789	723,287,507	735,954,540	229,417,080
Win17	2	943	56,006	1,673,044	23,301,353	167,641,976	623,185,078	1,149,259,314	929,917,134	239,415,886
Lose18	0	79	9,208	381,082	7,234,231	66,716,679	312,537,574	719,105,452	718,302,156	220,915,405
Win19	3	880	54,447	1,580,866	22,074,687	159,783,115	598,221,221	1,106,692,046	893,897,075	228,304,085
Lose20	0	92	10,286	422,820	7,648,246	68,172,135	312,429,372	709,620,858	703,347,268	214,981,695
Win21	10	764	51,850	1,484,500	20,654,257	150,217,223	566,745,403	1,057,372,471	860,316,258	220,406,392
Lose22	0	116	11,689	450,444	7,826,713	67,802,433	305,396,780	688,017,416	679,840,815	207,881,642
Win23	3	860	47,838	1,369,776	18,987,980	138,815,936	527,550,780	994,151,768	817,254,024	211,016,486
Lose24	0	176	12,735	463,790	7,755,272	65,702,045	291,746,213	653,134,789	644,727,337	197,610,370
Win25	7	883	44,703	1,240,426	17,194,038	126,125,526	482,359,048	917,271,786	762,448,425	199,022,358
Lose26	0	194	13,314	456,983	7,432,674	62,030,648	272,690,120	608,001,415	600,184,051	184,715,311
Win27	6	848	40,020	1,110,779	15,341,013	112,856,568	434,214,358	832,490,005	699,074,500	184,801,533
Lose28	0	208	12,953	434,483	6,956,148	57,300,432	250,484,458	557,242,112	550,489,523	170,182,516
Win29	3	723	35,120	977,979	13,537,945	99,850,700	386,459,960	746,831,950	633,559,139	169,533,289
Lose30	0	208	12,370	407,742	6,393,332	52,201,309	227,296,431	505,325,378	499,875,049	155,196,355
Win31	4	658	31,386	861,475	11,872,844	87,816,425	341,644,155	665,155,955	569,769,534	154,141,932
Lose32	0	219	11,799	375,196	5,803,695	47,089,410	204,587,712	455,117,090	451,095,010	140,525,090
Win33	4	563	27,245	751,656	10,365,271	76,870,278	300,722,279	589,852,418	509,714,325	139,209,587
Lose34	0	186	10,959	340,015	5,213,248	42,116,952	182,981,055	407,680,306	404,984,298	126,497,991
Win35	5	497	24,381	655,402	9,021,096	67,139,871	264,086,061	521,561,175	454,242,522	124,984,458
Lose36	0	200	10,118	305,275	4,640,486	37,471,738	162,953,527	363,830,752	362,217,256	113,327,285
Win37	7	517	20,891	566,785	7,826,871	58,531,770	231,532,694	460,218,877	403,461,768	111,723,902
Lose38	5	206	9,360	272,178	4,111,323	33,194,200	144,709,526	323,948,548	322,890,817	101,165,489
Win39	6	419	18,729	490,617	6,789,778	50,962,129	202,804,167	405,628,883	357,609,465	99,470,460
Lose40	3	150	8,133	243,353	3,635,425	29,368,107	128,346,807	287,907,437	287,405,365	89,997,042
Win41	2	332	15,672	425,983	5,907,222	44,487,375	177,801,407	357,248,055	316,537,202	88,425,914
Lose42	3	137	7,034	214,499	3,224,176	26,019,681	113,703,300	255,430,333	255,272,595	79,988,481
Win43	2	300	13,698	370,850	5,149,856	38,889,535	155,926,748	314,596,793	279,764,212	78,380,813
Lose44	0	113	6,512	191,096	2,851,977	23,002,098	100,654,805	226,330,963	226,270,901	70,912,978
Win45	2	272	11,900	322,511	4,484,007	33,985,670	136,819,888	277,015,126	247,083,688	69,415,874
Lose46	0	120	5,764	169,399	2,517,975	20,314,984	89,063,911	200,380,908	200,422,945	62,807,678
Win47	0	235	10,163	280,535	3,912,411	29,758,088	120,170,611	244,046,255	218,334,875	61,498,840
Lose48	1	106	5,167	149,013	2,221,367	17,945,656	78,742,162	177,353,530	177,502,150	55,613,738
Win49	0	198	8,992	244,231	3,417,906	26,061,024	105,614,857	215,105,686	192,916,913	54,483,681
Lose50	1	80	4,622	130,968	1,957,610	15,840,681	69,635,159	157,000,541	157,173,051	49,265,495
Win51	0	176	7,897	213,278	2,993,348	22,865,671	92,959,840	189,849,582	170,650,303	48,300,910
Lose52	0	97	3,961	115,308	1,728,224	14,003,502	61,683,585	139,125,334	139,253,562	43,628,882
Win53	0	165	7,020	186,125	2,625,777	20,126,920	82,051,422	167,840,151	151,169,176	42,839,774
Lose54	1	67	3,474	102,352	1,527,898	12,413,104	54,697,322	123,472,824	123,552,051	38,689,107
Win55	2	150	5,942	163,933	2,313,128	17,770,031	72,547,951	148,618,217	134,015,932	38,052,231
Lose56	0	58	3,131	91,032	1,355,987	11,025,047	48,598,124	109,699,460	109,719,280	34,362,424
Win57	1	110	5,393	146,020	2,045,085	15,719,585	64,234,596	131,813,933	119,003,201	33,852,239
Lose58	0	58	2,755	81,259	1,209,449	9,812,466	43,255,672	97,589,357	97,562,544	30,567,467
Win59	1	112	4,650	128,772	1,812,336	13,936,401	56,985,409	117,065,950	105,881,414	30,162,382
Lose60	0	51	2,447	71,143	1,074,746	8,740,338	38,534,857	86,995,053	86,988,746	27,242,731
Win61	0	106	4,122	114,210	1,609,378	12,397,938	50,734,770	104,327,626	94,433,994	26,964,354
Lose62	0	51	2,213	64,198	960,947	7,819,619	34,463,604	77,769,677	77,687,146	24,323,524
Win63	0	94	3,788	103,198	1,437,345	11,064,936	45,307,756	93,230,793	84,422,438	24,089,828
Lose64	0	37	1,875	58,421	864,288	7,008,107	30,870,894	69,621,079	69,486,034	21,726,894
Win65	0	62	3,335	92,149	1,287,301	9,895,163	40,516,197	83,399,154	75,549,781	21,606,653
Lose66	0	28	1,733	51,979	776,805	6,287,684	27,678,883	62,372,044	62,197,829	19,439,682
Win67	0	70	3,016	81,652	1,151,275	8,850,489	36,256,546	74,663,401	67,668,983	19,350,022
Lose68	0	31	1,547	46,627	696,355	5,641,204	24,826,926	55,922,253	55,722,587	17,418,538
Win69	0	69	2,675	73,729	1,030,592	7,936,316	32,509,472	66,963,324	60,709,938	17,373,780
Lose70	0	23	1,409	42,166	624,806	5,068,247	22,296,208	50,192,632	49,997,724	15,617,654
Win71	2	60	2,489	65,718	923,963	7,113,896	29,149,556	60,063,716	54,533,069	15,620,522
Lose72	1	27	1,256	37,575	560,295	4,547,864	20,012,343	45,052,681	44,901,335	14,029,767
Win73	1	47	2,104	59,021	828,060	6,379,003	26,162,054	53,890,542	48,947,648	14,050,217
Lose74	0	21	1,104	34,070	501,708	4,082,644	17,963,436	40,439,692	40,277,825	12,581,156
Win75	0	43	1,839	53,320	741,617	5,722,479	23,464,793	48,375,680	43,946,373	12,591,326
Lose76	0	13	1,027	30,201	448,281	3,656,371	16,115,877	36,328,321	36,186,937	11,285,566
Win77	0	38	1,710	46,252	662,231	5,115,602	21,036,065	43,447,414	39,511,494	11,334,564
Lose78	1	13	868	26,541	400,953	3,273,733	14,467,958	32,624,442	32,523,582	10,152,784
Win79	0	26	1,476	41,431	591,157	4,583,549	18,883,196	39,030,857	35,553,873	10,199,664
Lose80	0	9	792	23,807	360,308	2,939,844	13,017,618	29,394,542	29,307,114	9,147,322
Win81	0	36	1,340	37,334	531,498	4,110,564	16,966,776	35,126,598	32,018,925	9,211,442
Lose82	0	11	788	21,355	323,573	2,638,531	11,708,296	26,469,462	26,393,881	8,245,240
Win83	1	39	1,162	33,390	474,647	3,690,659	15,263,658	31,633,538	28,842,447	8,293,676
Lose84	0	10	649	19,171	288,515	2,369,329	10,525,765	23,817,072	23,761,621	7,419,103
Win85	1	22	1,077	29,722	425,461	3,322,866	13,722,346	28,457,972	25,972,344	7,467,978
Lose86	0	15	606	17,313	259,875	2,131,677	9,451,938	21,404,708	21,354,859	6,668,303
Win87	1	23	964	27,382	384,218	2,978,193	12,311,956	25,573,975	23,364,846	6,732,662
Lose88	0	11	540	15,450	234,998	1,910,951	8,482,606	19,220,016	19,191,536	6,001,512
Win89	0	14	845	24,178	344,225	2,673,264	11,058,773	22,971,605	21,010,385	6,056,258
Lose90	0	9	465	13,729	210,213	1,715,887	7,615,118	17,252,471	17,234,231	5,385,603
Win91	0	13	751	21,220	307,872	2,395,136	9,929,886	20,632,779	18,878,049	5,435,897
Lose92	0	8	395	12,129	187,853	1,537,362	6,833,760	15,493,489	15,480,740	4,839,579
Win93	0	10	624	19,072	274,103	2,145,021	8,911,390	18,536,930	16,974,073	4,890,022
Lose94	0	7	334	10,946	167,920	1,379,676	6,142,259	13,929,966	13,919,035	4,342,129
Win95	1	13	585	16,753	246,772	1,933,072	8,013,932	16,671,765	15,281,717	4,412,577
Lose96	0	6	311	9,916	151,588	1,240,906	5,527,559	12,545,184	12,537,834	3,923,222
Win97	0	10	494	15,446	224,472	1,747,337	7,224,772	15,052,831	13,789,222	3,980,511
Lose98	0	4	308	9,204	139,318	1,128,968	5,005,395	11,332,545	11,310,904	3,531,177
Win99	0	8	486	14,603	206,202	1,585,794	6,544,890	13,590,344	12,453,647	3,598,607
Lose100	0	9	308	8,496	126,722	1,029,298	4,543,552	10,242,372	10,220,901	3,199,217

(2023/3/9 現在)
キリのいいところまで解析したので中断しました。

後退解析とは？

突然ですが、一手詰めの詰将棋を考えてみます。これは「どのような手を指せば相手を詰ませられるか？」という問題です。つまり一手詰めの局面とは「うまい手を選べば、その次の相手の局面が詰み局面となっている」を満たす局面です。いわば詰み局面の一手前を見つける作業に該当します。
一手詰めの局面がすべて列挙できれば、次に「どんな手を選んだとしても、次の相手の局面は一手詰めの局面か、一手で相手が勝てる局面になる」という局面について考えられます。これも一手詰め局面から一手前に戻った局面に該当します。こんな言葉はないですが、いわば「二手詰まされ」の局面です。
上記の探索を繰り返すと
詰み→一手詰め→二手詰まされ→三手詰め→四手詰まされ→...
のようにして、両者が最善手を選び続けた場合に勝敗が確定した局面をどんどん列挙することができます。*1

局面の分類

いずれの組のボスハトも包囲されていない局面を分類することを考えます。両方のボスハトが同時に包囲された局面に至った場合はその手を指したプレイヤーが負けというルールを採用します。別の言い方をすれば「同時にボスハトが囲まれる局面は禁止」と考えればより分かりやすいかもしれません。
ある局面を考えて、ルール上可能な手を選んだ結果としては以下の可能性があります:

ゲーム続行
そのプレーヤーが勝ち
そのプレイヤーが負け

このうち上二つのいずれかの手がどんな局面でも必ず存在することは以下の記事ですでに確かめました。
smooth-pudding.hatenablog.com
実行するとゲーム続行となる手を「続行手」、実行するとそのプレイヤーが勝つ手を「勝利手」と呼ぶこととします。以下では、その手を実行するとそのプレイヤーが負けとなる手は考えても意味がないので無視します。
もし可能な手に勝利手が含まれているなら、それを選べば勝つのですから、当然その手を選ぶべきでしょう。このような局面をWin1局面と呼ぶこととします。
次に、その局面で選べる手が続行手しかない場合を考えます。もし「どの続行手を選んだとしても、その結果が直後の相手にとってすべてWin1局面である」という状況ならば、両者が最善手を選べば残り二手でゲームが終了します（最初のプレイヤーの敗北）。このような局面をLose2局面と呼ぶこととします。Lose2局面はちょうど将棋でいう「詰み」と同等です。
今度はその局面で選べる手が続行手しかない場合で、「ある続行手を選べば、その結果が直後の相手にとってLose2局面である」という手があるような場合を考えます。この手を選ぶこと、その後両者が最善手を選べばトータルで三手でゲームが終了することになります（最初のプレイヤーの勝利）。この局面をWin3局面と呼ぶこととします。
もうすこし続けます。その局面で選べる手が続行手しかない場合で、「どの続行手を選んだとしても、その結果が直後の相手にとってすべてWin1またはWin3局面である」が成り立ち、さらにその局面がLose2局面でないことが分かっているとします。つまりある手を選べば、その結果が直後の相手にとってWin3局面になる、という状況です。Win1局面になる手よりかは終了までのターン数が稼げるので、よりよい手、という風に考えることにします。このような局面をLose4局面と呼ぶこととします。
同じように、その局面で選べる手が続行手しかない場合で、「ある続行手を選べば、その結果が直後の相手にとってLose4局面である」が成り立ち、さらにその局面がWin3局面でないことが分かっているとします。つまり、どんな手を選んだとしても、その結果が直後の相手にとってLose2局面となることはない、という状況です。なるべく短いターン数で終わらせるのがよりよい手、という風に考えれば、直後がLose4局面になる手が最善手となります。このような局面をWin5局面と呼ぶこととします。
以下これを続けてLose6局面、Win7局面、Lose8局面、Win9局面、・・・と定義していきます。この結果

Win n 局面:
両者が最善手を指すと、n 手でゲームが終了する（手番プレイヤーの勝利）
Lose n 局面:
両者が最善手を指すと、n 手でゲームが終了する（手番プレイヤーの敗北）

となります。
すべての局面がこれらのいずれかに分類されるかどうかは分かりませんが、複数のものにまたがって属することはありません。もし初期局面が Win n や Lose n に属することが分かれば、このゲームは先手必勝または後手必勝であることがわかります*2。そこで、Win n, Lose n に属する局面を各 n に対して全列挙したい、となるわけです。
ちなみにいわゆる「詰将棋」に対応する「詰めハト」を考えるのであれば、Win3 が「一手詰め」、Win5が「三手詰め」、Win7が「五手詰め」・・・という風に、Win n 局面が「(n-2) 手詰め」となります。全列挙が完了していれば、そのうち Win n のものから適当に取り出せば詰めハトとなります。詰めハトの面白い問題はまた別記事で紹介したいです。

局面の分類の全列挙

前回の記事で、詰み局面を全列挙しました↓
smooth-pudding.hatenablog.com
これは今回の言葉を用いれば Lose2 局面の全列挙を行ったことになります。これをスタートにして、Win3, Lose4, Win5, Lose6, ... を全列挙する方法を説明します。

Lose から Win を列挙する方法

まず Lose n の全列挙が完了している場合を考えて、Win (n+1) を全列挙する方法を考えます。そのためには $1 \leq k \leq n$ を満たす各奇数kに対し、Win k に属するかどうかを判定できている必要があります。以下で説明する方法を用いればこれは自動的に達成される（順番に全列挙するため）ので、ここではすでに判定法を知っているものとします。
まず Lose n の各局面に対して、「ある合法手を実行するとその局面になる」という局面を列挙します。こう言うと少し列挙が難しそうですが、よくよく考えると「逆向きの合法手」を考えることで比較的簡単に列挙することができます。逆向きの合法手とは、以下を満たすものです:

ハトを動かす:
通常の合法手と同様
ハトを取り除く:
自軍に隣接しており、相手のボスの上下左右にないハトのみ取り除ける。どのハトも孤立してはいけない。
ハトを置く:
いずれかのハトに接していればOK

微妙に合法判定が違うものの、それほど順方向と複雑度は大差ありません。ひとつだけ要注意なのは、逆方向の手では、順方向の手番プレイヤーの対戦相手が動かすという点です。それ以外は簡単ですね。
一手戻しの全列挙に成功したら、これらのうち Win k ( $1 \leq k \leq n$ ) 局面のものを取り除きます。これは Win (n+1) 局面になりえないためです。残ったものはすべて Win (n+1) 局面となります。「適切な手を指せば、その結果が Lose n 局面になる。他の手を指してもゲーム終了手数を短くすることはできない。」という条件を満たすので、まさしく Win (n+1) 局面です。

Win から Lose を列挙する方法

次に Win n 局面の全列挙が完了しているとして Lose (n+1) 局面の全列挙を行う方法を説明します。先ほどと同様、Win k 局面 ( $1 \leq k \leq n$ ) であるかどうかを判定する方法はすでに知っているものとします。
Lose から Win を列挙したときと同様に、各 Win n 局面から出発して、一手戻した局面を全列挙します。さらにここから各 Win k 局面 ( $1 \leq k \leq n$ ) を取り除きます。Lose から Win を作ったときはこの時点で完了でしたが、Win から Lose を作る場合はもうひと手間必要です。
上記の要領で間引いた局面たちが Lose (n+1) 局面かどうか、さらに審査します。具体的には、各局面について、すべての順方向の合法手の結果の局面を調べ、それらが Win k ( $1 \leq k \leq n$ ) のいずれかに属することを確認します。すなわち「どうあがいても (n+1) 手以内に負ける」かどうかを判定します。この審査をクリアできたものだけを集めれば、晴れて Lose (n+1) 局面の全列挙完了です。
ちなみに「もっと短い手数で負けてしまう (つまりある $m < n$ なる m について Lose m 局面である）場合をチェックしなくてよいのか？」と気になる方もいると思います。このチェックが実は必要ないことは、これはこの候補の局面の作られ方を考えれば分かります。そもそも Win n の局面から逆方向に一手指して作った局面なので、順方向の手で Win n 局面になるものが存在することが保証されている、という訳です。

まとめ

以上、この記事では後退解析によって局面の分類を進めていく方法について紹介しました。解析は進行中なので、表の方は随時アップデートしようと思います。
実は3回ほどコードのバグが原因でやりなおしています。今度こそちゃんと列挙できていると信じたいところです*3。
手元の計算環境だと Win→Lose が26時間ほど、Lose→Win が4時間ほどかかるので、2ステップ進めるのに30時間かかります。また Win31 あたりまで行くとメモリが枯渇（80GB積んでいるんですが・・・）してくるのですが、直近の一回前にやったバグあり計算だと初期局面に到達できるかどうかはまだもう少しかかりそうだったので、メモリ増設だったりデータ並列の量を増やしたりを検討しています。でもこれ以上データ並列しちゃうともっと時間かかるのが悩みどころですが・・・。とりあえずこの記事の投稿時点から2,3週間経てば前回の Win31 ぐらいまではたどり着けるので、その先はまたそのとき考えます。
今度は詰めハトをいくつか紹介したいです。が気が変わったらまた別のテーマかもです？
ではまた。

*1:一般には、「後退解析」はもうすこし広い意味で用いるようです。例えば以下のページではこの記事で調べている解析はもはや後退解析とは呼ばず、引き分けの処理を含めたものを後退解析と呼ぶ、という風にも読めます。
ゲームを解く！Educational DP Contest K, L 問題の解説 - Qiita
正直私はこの分野に関して素人なので用語法はイマイチかもしれませんが、とりあえずここでは上で説明した解析を「後退解析」と呼ぶことにします。

*2:前にどこか別の記事でも触れた気がしますが、初期配置からボスハトを斜めに動かす手が合法なため、実は初期配置が Lose に属さないことはすぐわかります。

*3:追試してくださる有志の方いませんか・・・いませんよね・・・