将棋の最大分岐数（すべての局面における合法手の数の最大値）は593であることが証明されています。
http://www.nara-wu.ac.jp/math/personal/shinoda/bunki.html
この証明は実際の局面を構成してはいませんが、簡単に構成可能でして、やっている人がいます。
この局面は実戦では出にくい気がしますが、でも両プレイヤーが協力して合法手を指していけば到達可能な局面ではあります。将棋は持ち駒を打てるので、大抵の局面は協力すれば到達可能な気がします。しかし詰将棋界隈ではこの（対局開始局面から詰将棋問題の局面への）到達可能性が満たされているかはトピックになっていて、かつややこしいケースがあるっぽいです。
オセロの最大分岐数はいくらなんでしょうか？ edaxは合法手の数が32以下であることを仮定してデータ構造を組んでいますが、本当にそうなのか疑問に思ったので調べてみました。
オセロの最大分岐数の上界をSMTソルバーで求める
z3を使い、手番側と相手の石のビットボード(64bit整数2つ)が任意の値を取れるとして、制約条件として
- 両プレイヤーの石が同じマスに置かれてはいけない
- 真ん中の4箇所には必ず石が置かれている
- 合法手の数がn個以上である
- 空白マスの数がk個以上である
としました。nとkを増やしていってunsatになったら終了としました。
合法手の数を計算する方法ですが、edaxの合法手生成とpopcountは以下のように分岐なし・ビット演算と四則演算だけで書かれているので、z3にベタに落とし込めます。ちなみに、z3の右シフト演算子は算術シフトなので注意しましょう。
https://github.com/abulmo/edax-reversi/blob/master/src/board.c
static inline unsigned long long get_some_moves(const unsigned long long P, const unsigned long long mask, const int dir) { register unsigned long long flip_l, flip_r; register unsigned long long mask_l, mask_r; const int dir2 = dir + dir; flip_l = mask & (P << dir); flip_r = mask & (P >> dir); flip_l |= mask & (flip_l << dir); flip_r |= mask & (flip_r >> dir); mask_l = mask & (mask << dir); mask_r = mask & (mask >> dir); flip_l |= mask_l & (flip_l << dir2); flip_r |= mask_r & (flip_r >> dir2); flip_l |= mask_l & (flip_l << dir2); flip_r |= mask_r & (flip_r >> dir2); return (flip_l << dir) | (flip_r >> dir); } unsigned long long get_moves(const unsigned long long P, const unsigned long long O) { const unsigned long long mask = O & 0x7E7E7E7E7E7E7E7Eull; return (get_some_moves(P, mask, 1) // horizontal | get_some_moves(P, O, 8) // vertical | get_some_moves(P, mask, 7) // diagonals | get_some_moves(P, mask, 9)) & ~(P|O); // mask with empties }
https://github.com/abulmo/edax-reversi/blob/master/src/bit.c
int bit_count(unsigned long long b) { register unsigned long long c = b - ((b >> 1) & 0x7777777777777777ULL) - ((b >> 2) & 0x3333333333333333ULL) - ((b >> 3) & 0x1111111111111111ULL); c = ((c + (c >> 4)) & 0x0F0F0F0F0F0F0F0FULL) * 0x0101010101010101ULL; return (int)(c >> 56); }
結果
合法手の数が35通り以上の局面は存在しないことが証明できました。また、合法手の数が34通りで、かつ空白が38箇所以上ある局面も存在しないことが証明できました。以下は見つけた例で、分岐数34で37マス空きです。（黒の手番です）
これが対局開始局面から合法手のみで到達可能かどうかはよくわかりませんが怪しい気がしています。
コード
import time import re import sys import z3 # z3をimportする簡単な方法： # https://qiita.com/SatoshiTerasaki/items/476c9938479a4bfdda52 def print_board(player, opponent, move): print(" A B C D E F G H") for i in range(8): print(str(i+1) + " ", end = "") for j in range(8): if (player & (1 << (i * 8 + j))) > 0: print("* ", end = "") elif (opponent & (1 << (i * 8 + j))) > 0: print("o ", end = "") elif (move & (1 << (i * 8 + j))) > 0: print(". ", end = "") else: print("- ", end = "") print(i+1, end = "") if i == 2: print(" * = player's disc", end = "") elif i == 3: print(" o = opponent's disc", end = "") elif i == 4: print(" - = empty, illegal move", end = "") elif i == 5: print(" . = empty, legal move", end = "") print("") print(" A B C D E F G H") def solve(movenum, emptynum): bb_player = z3.BitVec("bb_player", 64) bb_opponent = z3.BitVec("bb_opponent", 64) bb_occupied = z3.BitVec("bb_occupied", 64) bb_empty = z3.BitVec("bb_empty", 64) masked_bb_opponent = z3.BitVec("masked_bb_opponent", 64) movemask = [z3.BitVec(f"movemask_{i}", 64) for i in range(4)] directions1 = [z3.BitVec(f"directions1_{i}", 64) for i in range(4)] directions2 = [z3.BitVec(f"directions2_{i}", 64) for i in range(4)] flip_l_0 = [z3.BitVec(f"flip_l_0_{i}", 64) for i in range(4)] flip_r_0 = [z3.BitVec(f"flip_r_0_{i}", 64) for i in range(4)] flip_l_1 = [z3.BitVec(f"flip_l_1_{i}", 64) for i in range(4)] flip_r_1 = [z3.BitVec(f"flip_r_1_{i}", 64) for i in range(4)] flip_l_2 = [z3.BitVec(f"flip_l_2_{i}", 64) for i in range(4)] flip_r_2 = [z3.BitVec(f"flip_r_2_{i}", 64) for i in range(4)] flip_l_3 = [z3.BitVec(f"flip_l_3_{i}", 64) for i in range(4)] flip_r_3 = [z3.BitVec(f"flip_r_3_{i}", 64) for i in range(4)] mask_l = [z3.BitVec(f"mask_l_{i}", 64) for i in range(4)] mask_r = [z3.BitVec(f"mask_r_{i}", 64) for i in range(4)] some_moves = [z3.BitVec(f"some_moves_{i}", 64) for i in range(4)] all_moves = z3.BitVec("all_moves", 64) popcnt_move_tmp1 = z3.BitVec("popcnt_move_tmp1", 64) popcnt_move_tmp2 = z3.BitVec("popcnt_move_tmp2", 64) pop_move = z3.BitVec("pop_move", 64) popcnt_empty_tmp1 = z3.BitVec("popcnt_empty_tmp1", 64) popcnt_empty_tmp2 = z3.BitVec("popcnt_empty_tmp2", 64) pop_empty = z3.BitVec("pop_empty", 64) s = z3.Solver() s.add( (bb_player & bb_opponent) == 0, bb_occupied == bb_player | bb_opponent, bb_empty == bb_occupied ^ 0xFFFFFFFFFFFFFFFF, (bb_occupied & 0x0000001818000000) == 0x0000001818000000, masked_bb_opponent == bb_opponent & 0x7E7E7E7E7E7E7E7E, movemask[0] == masked_bb_opponent, movemask[1] == masked_bb_opponent, movemask[2] == bb_opponent, movemask[3] == masked_bb_opponent, directions1[0] == 1, directions1[1] == 7, directions1[2] == 8, directions1[3] == 9, directions2[0] == 2, directions2[1] == 14, directions2[2] == 16, directions2[3] == 18 ) s.add([z3.And(flip_l_0[i] == (movemask[i] & (bb_player << directions1[i]))) for i in range(4)]) s.add([z3.And(flip_r_0[i] == (movemask[i] & z3.LShR(bb_player, directions1[i]))) for i in range(4)]) s.add([z3.And(flip_l_1[i] == (flip_l_0[i] | (movemask[i] & (flip_l_0[i] << directions1[i])))) for i in range(4)]) s.add([z3.And(flip_r_1[i] == (flip_r_0[i] | (movemask[i] & z3.LShR(flip_r_0[i], directions1[i])))) for i in range(4)]) s.add([z3.And(mask_l[i] == (movemask[i] & (movemask[i] << directions1[i]))) for i in range(4)]) s.add([z3.And(mask_r[i] == (movemask[i] & z3.LShR(movemask[i], directions1[i]))) for i in range(4)]) s.add([z3.And(flip_l_2[i] == (flip_l_1[i] | (mask_l[i] & (flip_l_1[i] << directions2[i])))) for i in range(4)]) s.add([z3.And(flip_r_2[i] == (flip_r_1[i] | (mask_r[i] & z3.LShR(flip_r_1[i], directions2[i])))) for i in range(4)]) s.add([z3.And(flip_l_3[i] == (flip_l_2[i] | (mask_l[i] & (flip_l_2[i] << directions2[i])))) for i in range(4)]) s.add([z3.And(flip_r_3[i] == (flip_r_2[i] | (mask_r[i] & z3.LShR(flip_r_2[i], directions2[i])))) for i in range(4)]) s.add([z3.And(some_moves[i] == ((flip_l_3[i] << directions1[i]) | z3.LShR(flip_r_3[i], directions1[i]))) for i in range(4)]) s.add( all_moves == (some_moves[0] | some_moves[1] | some_moves[2] | some_moves[3]) & bb_empty, popcnt_move_tmp1 == all_moves - (z3.LShR(all_moves, 1) & 0x7777777777777777) - (z3.LShR(all_moves, 2) & 0x3333333333333333) - (z3.LShR(all_moves, 3) & 0x1111111111111111), popcnt_move_tmp2 == ((popcnt_move_tmp1 + z3.LShR(popcnt_move_tmp1, 4)) & 0x0F0F0F0F0F0F0F0F) * 0x0101010101010101, pop_move == z3.LShR(popcnt_move_tmp2, 56), pop_move >= movenum ) s.add( popcnt_empty_tmp1 == bb_empty - (z3.LShR(bb_empty, 1) & 0x7777777777777777) - (z3.LShR(bb_empty, 2) & 0x3333333333333333) - (z3.LShR(bb_empty, 3) & 0x1111111111111111), popcnt_empty_tmp2 == ((popcnt_empty_tmp1 + z3.LShR(popcnt_empty_tmp1, 4)) & 0x0F0F0F0F0F0F0F0F) * 0x0101010101010101, pop_empty == z3.LShR(popcnt_empty_tmp2, 56), pop_empty >= emptynum ) time_start = time.time() result = s.check() time_end = time.time() print(f"board: {movenum} or more moves, {emptynum} or more empties: {result}. elapsed time = {int(time_end - time_start)} second") if result == z3.unsat: return False satlist = sorted([x.strip() for x in str(s.model())[1:-1].split(",")]) # ['all_moves = 18446744073709551615', 'bb_empty = 8', ... satlist = [x.split(" = ") for x in satlist if re.match(r"^(all_moves|bb_player|bb_opponent) = ", x.strip()) is not None] for x in satlist: print(x[0] + "".join([" " for _ in range(11 - len(x[0]))]) + " = " + format(int(x[1]), "#066b")) print_board(int([x for x in satlist if "player" in x[0]][0][1]),int([x for x in satlist if "opponent" in x[0]][0][1]),int([x for x in satlist if "moves" in x[0]][0][1])) return True if __name__ == "__main__": for i in range(1,61): b = solve(i, i) if b == False: for j in range(i,61): b = solve(i-1, j) if b == False: sys.exit(0)
