ナンバーリンク ― 数字のペアを回路でつなぐ

この章で学ぶこと

Z3 の章では、ナンバーリンクを「マスの値」と「線」の制約で解きました。CP-SAT には add_circuit() があるので、数字のペアを1つの回路として表せます。

• 数字のペアごとに、自己ループ付きの回路を作る

• 各マスは、どれか1つの回路にだけ属する

• 回路の経路を get_circuit() で取り出す

import numpy as np
from ortools.sat.python import cp_model
from helper.ortools import get_circuit

盤面

0 が空きマス、1以上の数値がペアになる数字です。

board = np.loadtxt('data/numberlink01.txt', dtype=np.uint8)
print(board)

[[1 0 0 0 0 0 0 0 0 0]
 [0 0 0 0 0 0 0 0 5 0]
 [0 6 0 1 0 0 0 0 0 0]
 [0 0 0 0 0 4 3 0 0 0]
 [0 0 0 0 0 0 6 0 5 0]
 [0 8 0 3 0 0 0 0 0 0]
 [0 0 0 4 7 0 0 0 0 0]
 [0 0 0 0 0 0 2 0 8 0]
 [0 7 0 0 0 0 0 0 0 0]
 [0 0 0 0 0 0 0 0 0 2]]

考え方

数字のペアの数だけ回路を作ります。たとえば数字1のペアなら、その2マスを通る1本の回路です。

1. 各回路には、すべてのマスの有向辺と、各マスの自己ループを入れる

   • 自己ループ (i, i) は「このマスはこの回路に属さない」という意味

2. 数字のペア n1, n2 については、辺 (n2, n1) を必ず使う

   • これで、n2 → … → n1 の経路ができ、全体は1本の回路になる

3. 各マスについて、自己ループが偽になる回路はちょうど1つ

   • つまり、そのマスは1つの数字の経路にだけ属する

3のおかげで、線が交差したり、1つのマスを2つの数字が使ったりすることがありません。

マスと辺を作る

def create_nodes_edges(board):
    """各マスに番号を振り、隣り合うマス同士の有向辺を作る"""
    h, w = board.shape
    nodes = np.arange(w * h).reshape((h, w))
    edges = []
    for r in range(h):
        for c in range(w):
            node = nodes[r, c]
            if c + 1 < w:
                right = nodes[r, c + 1]
                edges.extend([(node, right), (right, node)])
            if r + 1 < h:
                bottom = nodes[r + 1, c]
                edges.extend([(node, bottom), (bottom, node)])
    return nodes, edges

解く

def solve_number_link(board):
    """ナンバーリンクを解いて (線, 各マスの数字) を返す"""
    h, w = board.shape
    model = cp_model.CpModel()
    nodes, edges = create_nodes_edges(board)

    number_starts = {}      # 数字 → 始点のマス番号
    layers_circuits = {}    # 数字 → 有向辺の変数
    layers_nodes = {}       # 数字 → 自己ループの変数

    for n in range(1, int(board.max()) + 1):
        r, c = np.where(board == n)
        node1 = nodes[r[0], c[0]]
        node2 = nodes[r[1], c[1]]

        circuit_variables = [(s, t, model.new_bool_var(f"{n}_{s}_{t}")) for s, t in edges]
        node_variables = [(s, s, model.new_bool_var(f"{n}_{s}_{s}")) for s in nodes.ravel()]

        # node2 → node1 を必ず通す（このペアをつなぐ回路にする）
        model.add_circuit(circuit_variables + node_variables + [(node2, node1, True)])

        number_starts[n] = node1
        layers_circuits[n] = circuit_variables
        layers_nodes[n] = node_variables

    # 各マスは、どれか1つの回路にだけ属する（自己ループが偽になるのは1つ）
    for node in nodes.ravel():
        variables = [value[node][2] for value in layers_nodes.values()]
        model.add_exactly_one([~v for v in variables])

    solver = cp_model.CpSolver()
    if solver.solve(model) not in (cp_model.OPTIMAL, cp_model.FEASIBLE):
        raise ValueError("解が見つかりませんでした")

    links = {}
    cells = {}
    for number, circuits in layers_circuits.items():
        solution = {(s, t): solver.value(v) for s, t, v in circuits}
        path = get_circuit(solution, start=number_starts[number])
        path = [(p // w, p % w) for p in path]
        for p in path:
            cells[p] = number
        for p1, p2 in zip(path[:-1], path[1:]):
            links[p1 + p2] = True
    return links, cells

実行

helper.plot.plot_number_link_board() で、盤面と解いた線を描きます。

from helper.plot import plot_number_link_board

links, cells = solve_number_link(board)
plot_number_link_board(board, links, cells);

複雑なパズル

%%time
board = np.loadtxt('data/numberlink02.txt', dtype=np.uint8)
links, cells = solve_number_link(board)
plot_number_link_board(board, links, cells);

CPU times: total: 9.48 s
Wall time: 2.35 s

検算

各数字の経路が、正しく2つの数字マスを結んでいるか確かめます。

def check_number_link(board, cells):
    """各数字の経路が、2つの数字マスを結ぶ1本の線になっているか"""
    groups = {}
    for pos, n in cells.items():
        groups.setdefault(n, set()).add(pos)

    for n in range(1, int(board.max()) + 1):
        group = groups.get(n, set())
        ends = {(r, c) for r, c in zip(*np.where(board == n))}
        if not ends <= group:
            return False, f"{n} の数字マスが経路に入っていません"

        # 連結か
        start = next(iter(group))
        seen = {start}
        stack = [start]
        while stack:
            r, c = stack.pop()
            for dr, dc in ((1, 0), (-1, 0), (0, 1), (0, -1)):
                nb = (r + dr, c + dc)
                if nb in group and nb not in seen:
                    seen.add(nb)
                    stack.append(nb)
        if seen != group:
            return False, f"{n} の経路が途切れています"

        # 端は2つだけ（それ以外は2本ずつつながる）
        degree = {}
        for (r, c) in group:
            degree[r, c] = sum(1 for dr, dc in ((1, 0), (-1, 0), (0, 1), (0, -1))
                               if (r + dr, c + dc) in group)
        if {p for p, d in degree.items() if d == 1} != ends:
            return False, f"{n} の経路の端が数字マスと一致しません"
        if any(d > 2 for d in degree.values()):
            return False, f"{n} の経路が枝分かれしています"

    return True, f"{int(board.max())} 本の経路がすべて正しくつながっています"


print(check_number_link(board, cells))

(True, '17 本の経路がすべて正しくつながっています')

まとめ

• 数字のペアごとに add_circuit() を作り、(n2, n1) を必ず通すと、その2マスを結ぶ経路になる

• 各マスに自己ループを用意し、「自己ループが偽になるのは1つだけ」とすれば、マスが1つの経路にだけ属する

• 番号が大きい方から小さい方へ戻る辺を固定するのがポイント（経路を開いた回路にする）

• Z3 で書いたとき（値と線の制約）より、コードが短く済む