<jupyter_start><jupyter_text>京都将棋の弱解決の検証(注) Notebook形式で作成してみましたが，Google Colab上ではメモリ不足で動きませんでした．64GB搭載の MacBook Pro上では動きます．この Notebookは[第26回ゲームプログラミングワークショップ GPW-2021](https://www.gi-ipsj.org/gpw/2021/) で [ベストポスター賞](https://www.gi-ipsj.org/gpw/2021/to_award.html)を受賞した電気通信大学の塩田 雅弘さん，伊藤 毅志さんによる[京都将棋の弱解決](https://ipsj.ixsq.nii.ac.jp/ej/?action=pages_view_main&active_action=repository_view_main_item_detail&item_id=213428&item_no=1&page_id=13&block_id=8)の発表の結果を検証するために作成しました．プログラムを動かすためには，塩田 雅弘さんの公開している [mate.7z](https://drive.google.com/file/d/1TBZk8t-jNfSb8eTKr5YftS9DAi5AYzsK/view?usp=sharing) を展開したファイル mate.db を同じディレクトリに置く必要があります．Notebookではなくてpythonファイル形式でダウンロードして pypy で動かすと1時間ほどで検証が終わると思います．ただし，この場合もメモリは32GB以上は必要と思われます．<jupyter_code>def str2board(s):
    ans = [[''] * 5 for _ in range(5)]
    for i, l in enumerate(s.split('/')):
        x = 0
        j = 0
        while x < 5:
            if l[j].isdigit():
                for k in range(int(l[j])):
                    ans[i][x + k] = ''
                x += int(l[j])
                j += 1
            else:
                if l[j] == '+':
                    ans[i][x] = l[j:(j + 2)]
                    j += 2
                else:
                    ans[i][x] = l[j]
                    j += 1
                x += 1
    return ans

def board2str(b):
    ans = []
    for y in range(5):
        l = []
        c = 0
        for x in range(5):
            if b[y][x] == '':
                c += 1
            else:
                if c > 0:
                    l.append(str(c))
                    c = 0
                l.append(b[y][x])
        if c > 0:
            l.append(str(c))
        ans.append(''.join(l))
    return '/'.join(ans)

pstr = 'snlpk'
pstrs = [''.join(c.upper() for c in pstr), pstr]

def str2hands(s):
    ans = [[0] * 5 for _ in range(2)]
    for i in range(2):
        for j, c in enumerate(pstr):
            if i == 0:
                c = c.upper()
            if c in s:
                k = s.index(c)
                if k > 0 and s[k - 1] == '2':
                    ans[i][j] = 2
                else:
                    ans[i][j] = 1
    return ans

def hands2str(hand):
    ans = []
    for i in range(2):
        for j in range(5):
            if hand[i][j] > 0:
                if hand[i][j] == 2:
                    ans.append('2')
                ans.append(pstrs[i][j])
    if len(ans) == 0:
        return '-'
    return ''.join(ans)


def str2turn(s):
    return 0 if s == 'b' else 1

def turn2str(turn):
    return 'bw'[turn]


def p2turn(p):
    if p == '':
        return ''
    elif p[-1].isupper():
        return 0
    return 1


def captured(p):
    p = p[-1]
    if p.isupper():
        return p.lower()
    return p.upper()


p2moves = {0 : {
    'L' : [(0, -1, 1)],
    '+L' : [(-1, -1, 0), (0, -1, 0), (1, -1, 0),(-1, 0, 0), (1, 0, 0),(0, 1, 0)],
    'S' : [(-1, -1, 0), (0, -1, 0), (1, -1, 0),(-1, 1, 0),(1, 1, 0)],
    '+S' : [(1, 1, 1), (1, -1, 1), (-1, 1, 1), (-1, -1, 1)],
    'K' : [(-1, -1, 0), (0, -1, 0), (1, -1, 0),(-1, 0, 0), (1, 0, 0), (-1, 1, 0),(0, 1, 0), (1, 1, 0)],
    'N' : [(-1, -2, 0), (1, -2, 0)],
    '+N' :  [(-1, -1, 0), (0, -1, 0), (1, -1, 0),(-1, 0, 0), (1, 0, 0),(0, 1, 0)],
    'P': [(0, -1, 0)],
    '+P' : [(0, -1, 1), (0, 1, 1), (1, 0, 1), (-1, 0, 1)]}}
p2moves[1] = {}
for p in p2moves[0]:
    wp = p.lower() if len(p) == 1 else '+' + p[1].lower()
    ms = [(x, -y, islong) for x, y, islong in p2moves[0][p]]
    p2moves[1][wp] = ms

ystr = 'abcde'
def c2x(c):
    return 5 - int(c)


def c2y(c):
    return ord(c) - ord('a')


def x2c(x):
    return str(5 - x)

def y2c(y):
    return ystr[y]


def makemove(x, y, x1, y1, p):
    pstr = '' if p.upper() == 'K' else ('-' if p[0] == '+' else '+')
    return f'{x2c(x)}{y2c(y)}{x2c(x1)}{y2c(y1)}{pstr}'

def makedrops(p, x, y):
    p = p[:-1] + p[-1].upper()
    m = f'{p}*{x2c(x)}{y2c(y)}'
    return [m, '+' + m]


def genmoves(pos):
    b, turn, hands = str2board(pos[0]), str2turn(pos[1]), str2hands(pos[2])
    #print('b', b, 'turn', turn, 'hands', hands)
    ans = []
    for y in range(5):
        for x in range(5):
            if b[y][x] == '':
                for i in range(5):
                    if hands[turn][i] > 0:
                        ans.extend(makedrops(pstrs[turn][i], x, y))
            elif p2turn(b[y][x]) == turn:
                #print('x,y,b[y][x],p2moves', (x, y, b[y][x]),p2moves[turn][b[y][x]])
                for dx, dy, islong in p2moves[turn][b[y][x]]:
                    x1, y1 = x + dx, y + dy
                    if islong:
                        while 0 <= x1 < 5 and 0 <= y1 < 5 and p2turn(b[y1][x1]) == '':
                            ans.append(makemove(x, y, x1, y1, b[y][x]))
                            x1 += dx
                            y1 += dy
                    if 0 <= x1 < 5 and 0 <= y1 < 5 and p2turn(b[y1][x1]) != turn:
                        ans.append(makemove(x, y, x1, y1, b[y][x]))
    return ans

def remove_from_hands(hands, p):
    op = p[1] if p[0] == '+' else p[0]
    newhands = [l[:] for l in hands]
    owner = 0 if op.isupper() else 1
    ptype = pstr.index(op.lower())
    assert hands[owner][ptype] > 0
    newhands[owner][ptype] -= 1
    return newhands


def add_to_hands(hands, p):
    newhands = [l[:] for l in hands]
    owner = 0 if p.isupper() else 1
    ptype = pstr.index(p.lower())
    assert hands[owner][ptype] < 2
    newhands[owner][ptype] += 1
    return newhands


def applymove(pos, move):
    b, turn, hands = str2board(pos[0]), str2turn(pos[1]), str2hands(pos[2])
    if '*' in move:
        x, y = c2x(move[-2]), c2y(move[-1])
        p = move[:2] if move[0] == '+' else move[0]
        b[y][x] = p if turn == 0 else p.lower()
        #print('pos, move', (pos, move, (p[-1] if turn == 0 else p[-1].lower())))
        hands = remove_from_hands(hands, p[-1] if turn == 0 else p[-1].lower())
    else:
        sx, sy = c2x(move[0]), c2y(move[1])
        dx, dy = c2x(move[2]), c2y(move[3])
        dp = b[dy][dx]
        if dp != '':
            hands = add_to_hands(hands, captured(dp))
        p = b[sy][sx]
        b[sy][sx] = ''
        afterp = '+' + p if len(p) == 1 and p not in 'kK' else p[-1]
        b[dy][dx] = afterp
    turn = 1 - turn
    return (board2str(b), turn2str(turn), hands2str(hands))


def is_check(b, turn):
    for y in range(5):
        for x in range(5):
            if p2turn(b[y][x]) == turn:
                #print('x,y,b[y][x],p2moves', (x, y, b[y][x]),p2moves[turn][b[y][x]])
                for dx, dy, islong in p2moves[turn][b[y][x]]:
                    x1, y1 = x + dx, y + dy
                    if islong:
                        while 0 <= x1 < 5 and 0 <= y1 < 5 and p2turn(b[y1][x1]) == '':
                            x1 += dx
                            y1 += dy
                    if 0 <= x1 < 5 and 0 <= y1 < 5 and p2turn(b[y1][x1]) != turn and b[y1][x1].lower() == 'k':
                        return True
    return False


def is_suicide_move(pos, move):
    newpos = applymove(pos, move)
    #print('newpos', newpos)
    turn = str2turn(newpos[1])
    b = str2board(newpos[0])
    return is_check(b, turn)


def genmoves_legal(pos):
    return [m for m in genmoves(pos) if not is_suicide_move(pos, m)]
def has_mate1(pos):
    moves = genmoves(pos)
    for m in moves:
        pos1 = applymove(pos, m)
        if not is_check(str2board(pos1[0]), str2turn(pos[1])):
            continue
        moves2 = genmoves_legal(pos1)
        if len(moves2) == 0:
            return True
    return False


def noescape(pos, depth):
    moves = genmoves_legal(pos)
    for m in moves:
        pos1 = applymove(pos, m)
        if not has_mate(pos1, depth - 1):
            return False
    return True


def has_mate(pos, depth):
    if depth <= 1:
        return has_mate1(pos)
    moves = genmoves(pos)
    for m in moves:
        pos1 = applymove(pos, m)
        if not is_check(str2board(pos1[0]), str2turn(pos[1])):
            continue
        if noescape(pos, depth - 1):
            return True
    return False
initpos = ('sfen p+nks+l/5/5/5/+LSK+NP', 'b', '-')<jupyter_output><empty_output><jupyter_text>データの読み込み塩田 雅弘さんに提供していただいた mate.7z ファイルを解凍すると mate.db というファイルが作成される．これを読み込む．``mate.db`` を読み込む．読み込んだ結果は以下のようになる* ``i2pos`` positionが並んだ配列* ``pos2i`` positionからi2posのindexを得るための連想配列* ``posmoves`` positionに対応するmovesの配列を保持する．なお，movesは[move, npos]の配列で，nposはmove後のpositionのindex以下のセルの実行時間は MacBook Pro(Apple M1 Max)で約2分<jupyter_code>import sys
pos2i = {}
i2pos = []
posmoves = []
with open('mate.db', 'r') as f:
    pos = None
    while l := f.readline():
        if len(l) > 0 and l[0] == '#':
            continue
        cs = l.split()
        if len(cs) > 0 and cs[0] == 'sfen':
            if len(cs) != 5 or cs[4] != '0' or cs[2] not in 'bw':
                print(l)
                continue
            pos = (cs[1], cs[2], cs[3])
            if pos in pos2i:
                print('dup', pos)
                continue
            pos2i[pos] = len(i2pos)
            i2pos.append(pos)
            posmoves.append([])
        else:
            if len(cs) != 3:
                print('invalid', cs)
                continue
            if pos[1] == 'w':
                if int(cs[2]) >= -30000:
                    print('invalid', cs)
                    continue
            else:
                if pos[1] == 'b':
                    if int(cs[2]) <= 30000:
                        print('invalid', cs)
                        continue
            posmoves[-1].append([cs[0], None])
n = len(i2pos)
print('len(i2pos)', n)
print('pos2i[initpos]', pos2i[initpos])
print('posmoves[pos2i[initpos]]', posmoves[pos2i[initpos]])<jupyter_output><empty_output><jupyter_text>初期配置は，```sfen p+nks+l/5/5/5/+LSK+NP b - 0```を ```initpos``` とする． initposから到達可能なグラフの構築をおこなう．これは，当初公開されていた mate.db で証明木(DAG)以外のノードが含まれていたため，それを除外するためである．** チェック1 ** whiteの手番で作成したmoveについては，かならずmove後のpositionがグラフに含まれる．なお，blackの手番ではmove後にwhiteの合法手がない場合はmove後のpositionはグラフに含まれない．以下のセルの実行時間はMacBook Pro(Apple M1 Max)で約14分<jupyter_code>g = [[] for _ in range(n)]
rg = [[] for _ in range(n)]
visited = [False] * n
def traverse(i):
    if visited[i]:
        return
    visited[i] = True
    pos = i2pos[i]
    for m in posmoves[i]:
        pos1 = applymove(pos, m[0])
        if pos1 in pos2i:
            j = pos2i[pos1]
            g[i].append(j)
            rg[j].append(i)
            m[1] = j
            traverse(j)
        else:
            if pos[1] == 'w':
                print('position after a white move is not found', (pos, m[0], pos1))
traverse(pos2i[initpos])


print(sum(visited), len(visited))<jupyter_output><empty_output><jupyter_text>DAGであることの確認グラフにサイクル (cycle) があると，千日手となる path を証明に含んでいることになる．これがないことを確認する．SCC (Strongly connected components) を求めても良いが，ないことの証明としては，葉から順にノードを取り除いていく方法で証明できる．以下のセルの実行には，MacBook Pro (Apple M1 Max)で約30秒<jupyter_code># cycleがないことの確認
rcounts = [len(g[i]) for i in range(n)]
q = [i for i in range(n) if rcounts[i] == 0 and visited[i]]
while len(q) > 0:
    i = q.pop()
    for j in rg[i]:
        rcounts[j] -= 1
        if rcounts[j] <= 0:
            q.append(j)
for i in range(n):
    if visited[i] and rcounts[i] > 0:
        print('i, pos', i, i2pos[i])<jupyter_output><empty_output><jupyter_text>** チェックポイント **- visited な black では，合法手が登録されている．行き先がない場合は，no escape- visited な white では，登録されている手の集合が，合法手の集合と等しいno escape のケースで，一手詰めとステイルメイト(stale mate, 王手はかかっていないが相手の合法手がない) がある．ステイルメイトは局面を記録することにする．以下のチェックプログラムの実行は数時間かかるが，無事に終了して証明木が正しいことがわかる．<jupyter_code>k1 = 0
sm = []
for i, pos in enumerate(i2pos):
    if i % 100000 == 0:
        print(i)
    if not visited[i]:
        continue
    moves = set(genmoves_legal(pos))
    if pos[1] == 'w':
        moves1 = set(m for m, j in posmoves[i])
        if moves != moves1:
            print('white movegen', (pos, moves, moves1))
    else:
        if posmoves[i][0][0] not in moves:
            print('invalid move', (pos, posmoves[i]))
        if len(posmoves[i]) != 1:
            print('black number moves', (pos, posmoves[i]))
        m = posmoves[i][0]
        if m[1] is None:
            pos1 = applymove(pos, m[0])
            if not noescape(pos1, 2):
                print('no mate', (pos, m, pos1))
            elif not is_check(str2board(pos1[0]), 0):
                sm.append(pos)
            else:
                k1 += 1

print(k1)
print(len(sm))<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.17367444112662417, 'fraction_numerical': 0.038334274876926804, 'mean_word_length': 1.9795623948064438, 'pattern_counts': {'":': 0, '<': 42, '<?xml version=': 0, '>': 32, 'https://': 4, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '5', 'dir': 'jupyter-structured-clean-dedup', 'id': '327306', 'license': 'Apache-2.0', 'n_tokens_mistral': 5648, 'n_tokens_neox': 5338, 'n_words': 1133, 'path': 'verify.ipynb', 'repo_name': 'tanakat01/verify_kyoto_shogi', 'size': '12391'}