第2章 Exact Coverで数独を解く¶

「4行7列へ2を置く」という候補を選ぶと、同時に四つの条件が決まります。そのマスには2が入り、 4行には2が一つ入り、7列にも2が一つ入り、そのマスを含む3×3ブロックにも2が一つ入ります。完成盤面は、このような候補を81個選び、数独の全条件をちょうど一度ずつ満たしたものです。

Exact Cover は、「選択肢の集合からいくつかを選び、すべての条件をちょうど一度ずつ満たす」問題です。数独をこの形へ変換すれば、数独専用の探索を記述することなく、汎用のExact Coverソルバーで解きます。

条件を一度ずつ覆う¶

まず、A、B、C、Dという四つの条件を考えます。選択肢は次の四行です。行に書かれた条件は、その行を選ぶと満たされます。

四列だけのExact Cover¶
選択肢	A	B	C	D
r1	1	0	1	0
r2	0	1	0	1
r3	1	0	0	1
r4	0	1	1	0

r1 と r2 を選べば、AからDまでの各列に1が一つずつ現れます。r3 と r4 も同じ条件を満たします。r1 と r3 はAを二重に覆うため、一緒には選べません。

$ python3 examples/05-exact-cover/toy.py

columns: A B C D
r1: A C
r2: B D
r3: A D
r4: B C
solutions: 2
solution 1: r1 r2
solution 2: r3 r4
nodes: 5
branches: 4

nodes は探索関数を呼んだ回数、branches は行を選んで試した回数です。この小例では、二つの解を得るまでに5回関数を呼び、四行を試しています。

集合の言葉を使うなら、全条件の集合を \(U\)、各選択肢が満たす条件の集合を \(S_1,S_2,\ldots\) とします。選んだ集合が互いに重ならず、その和集合が \(U\) になればExact Coverです。表では、条件を列、選択肢を行として表し、選んだ行の和が全成分1のベクトルになるようにします。

列を選び、使える行を試す¶

この0-1表からExact Coverを探索する基本手順が Algorithm X です。行を次の順序で選びます。

列が残っていなければ、全条件を覆えたので現在の行の組が解です。
残っている列から一つを選びます。
その列に1がある行を一つ選びます。
選んだ行が覆う列と、それらの列に1がある競合行を表から外します。
小さくなった表に同じ処理を適用します。

先ほどの表でA列を選ぶと、候補行は r1 と r3 です。r1 を試すとAとCが覆われ、 AまたはCに1がある r1、r3、r4 を以後の候補から外します。残ったBとDは r2 が覆うので、r1 と r2 が一つの解になります。r3 を試す枝からは、もう一つの解を探します。

ある列に1が一つもなければ、その条件を満たす選択肢が残っていません。その枝からは解を作れないので、直前に選んだ行へ戻って次を試します。

どの列から始めても、候補行を漏れなく試せば解は変わりません。サンプルでは、1の数が最も少ない列を選びます。選択肢が少ない条件から調べると、行き詰まりを早く見つけやすいためです。

def algorithm_x(
    rows: Mapping[RowId, Collection[ColumnId]],
    columns: Mapping[ColumnId, set[RowId]],
    limit: int,
    chosen: list[RowId],
    solutions: list[tuple[RowId, ...]],
    stats: SearchStats,
) -> bool:
    """解がlimit個集まったらTrue、探索を終えたらFalseを返す。"""
    stats.nodes += 1
    if not columns:
        # すべての列を一度ずつ覆えたので、選択した行が解になる。
        solutions.append(tuple(chosen))
        return len(solutions) >= limit

    # 選べる行が最も少ない列から調べ、早めに矛盾を見つける。
    column = min(columns, key=lambda item: (len(columns[item]), repr(item)))
    candidates = columns[column]
    if not candidates:
        stats.dead_ends += 1
        return False

    for row in sorted(candidates, key=repr):
        stats.branches += 1
        covered = rows[row]

        # 選んだ行と一つでも列を共有する行は、同時には選べない。
        conflicts = set().union(*(columns[item] for item in covered))
        next_columns = {
            item: available - conflicts
            for item, available in columns.items()
            if item not in covered
        }

        chosen.append(row)
        stop = algorithm_x(rows, next_columns, limit, chosen, solutions, stats)
        chosen.pop()
        if stop:
            return True

    return False

0と1を並べた表は作らず、columns を「条件列から、その列を覆える候補行の集合への対応」として持たせています。たとえば columns["A"] は、条件列Aに1がある候補行の集合です。候補行を一つ選ぶと、同じ条件列を覆う競合行を conflicts へ集め、残りの条件列から取り除きます。分岐ごとに辞書と集合を作り直すため、再帰から戻ると元の表がそのまま残っています。

この実装でも探索自体はバックトラックです。第1章「バックトラック」との違いは、探索関数がマス、行、列、ブロックの構造を意識しない点にあります。問題を「行で列を一度ずつ覆う」という共通形式に変換したあと、同じ algorithm_x() で一般例も数独も解きます。

数独を729行・324列へ変換する¶

空の9×9盤面では、「数独の行 \(r\)、列 \(c\) のマスへ数字 \(d\) を置く」という候補が \(9\times9\times9=729\) 通りあります。一つの候補をExact Cover表の一行にします。

Exact Cover表の条件列には、次の四種類の条件を置きます。それぞれ81列なので、合計は324列です。

数独の条件とExact Coverの列¶
列の種類	ちょうど一度満たす条件	列数
マス	各マスに数字を一つ置く	81
行・数字	各行で各数字を一度使う	81
列・数字	各列で各数字を一度使う	81
ブロック・数字	各3×3ブロックで各数字を一度使う	81

先ほどの「4行7列へ2を置く」という候補行には、次の四列だけ1が立ちます。

一つの候補行が覆う列¶
候補	マス	行・数字	列・数字	ブロック・数字
4行7列へ2	4行7列	4行の2	7列の2	6番ブロックの2

候補行を選ぶと、この四条件が同時に満たされます。同じマスへ別の数字を置く候補は「4行7列」の列で競合します。同じ行の別の場所へ2を置く候補は「4行の2」の列で競合します。列とブロックの重複も、残り二種類の列によって除かれます。

次のコードでは、マス、行、列、数字を0始まりで保持しています。本文の4行7列は、コードでは row == 3、column == 6 です。

def build_sudoku_model(givens: Board) -> SudokuModel:
    side, box_side = board_geometry(givens)
    columns: list[Constraint] = []
    for row in range(side):
        for column in range(side):
            columns.append(("cell", row, column))
    for unit in range(side):
        for digit in range(1, side + 1):
            columns.extend(
                [
                    ("row-digit", unit, digit),
                    ("column-digit", unit, digit),
                    ("box-digit", unit, digit),
                ]
            )

    rows: dict[Choice, tuple[Constraint, ...]] = {}
    for position, given in enumerate(givens):
        row, column = divmod(position, side)
        box = (row // box_side) * box_side + column // box_side
        digits = (given,) if given else range(1, side + 1)
        for digit in digits:
            # 「このマスへこの数字を置く」という候補は、四つの条件を覆う。
            rows[(row, column, digit)] = (
                ("cell", row, column),
                ("row-digit", row, digit),
                ("column-digit", column, digit),
                ("box-digit", box, digit),
            )

    return SudokuModel(rows, tuple(columns), side)

初期配置があるマスでは、与えられた数字の候補行だけを作ります。空きマスには1から9までの九行を作ります。この絞り込みにより、初期配置もExact Cover表へ反映されます。たとえば初期数字が一つあれば、空盤面の729行から、そのマスに入る残り八つの候補行が減ります。

実行する¶

完全なコードは examples/05-exact-cover/solve.py にあります。詳しい実行手順やオプションについては examples/05-exact-cover/README.md を参照してください。

candidate rows は初期配置を反映した候補行数、constraint columns は満たすべき列数です。 nodes は探索関数の呼び出し回数、branches は選んで試した行の数、dead ends は候補行が 0本の列を見つけた回数です。

通常問題¶

通常問題では529行・324列の表が構成され、解が一つ得られた後に全選択肢の探索が完了（exhausted: yes）し、本問題が一意解であることが確定します。

解がない問題¶

矛盾問題では、探索途中で候補行が存在しない列が発生する不能状態に至ります。別の行を選択する全分岐の走査を終えても解が存在しないため、解なし（unsat）を出力します。

解が複数ある問題¶

複数解問題では、互いに異なる二つの完成盤面が得られた時点で指定上限により探索を打ち切り、一意解ではない（複数解を持つ）ことが判定されます。いずれの盤面も共通検証器によって検証されます。

Algorithm XとDancing Links¶

この章の実装は、分岐ごとにPythonの辞書と集合をコピーします。処理の対応は読みやすいものの、大きな表ではコピーする要素が増えます。

Donald Knuthの公開プログラムにも使われている Dancing Links（DLX）は、疎な0-1表の1だけを循環双方向リストで結びます。列や行を外す操作はリンクのつなぎ替えで行い、逆順につなぎ直すと元の表へ戻せます。Algorithm Xの選択手順は変えず、表を外して戻す部分のデータ構造を置き換えた実装です [1]。

DLXまで実装すると、リンクを正しい順序で外し、逆順に戻すコードが説明の中心になります。この章ではExact Coverへの変換を見やすくするため、集合コピー版を採用しました。Pythonで Algorithm Xを実装し、数独などへ適用した例も報告されています [2]。

この方法で分かること¶

Algorithm Xが列を一つ選んだとき、Exact Coverはその列を覆う行を必ず一つ含みます。コードは該当する行をすべて分岐として試すため、途中で上限に達しない限り解を漏らしません。列がなくなれば解であり、候補行がない列があればその枝は失敗です。

全探索を終了して解が0個であれば unsat となります。一解のみ得て全探索を終了した場合は一意解、二解を得た時点で探索を打ち切った場合も一意解でないことが確定します。探索順序に乱数を用いていないため、同一のPython処理系であれば行の選択順序と探索回数を再現します。

Exact Coverソルバーが保証するのは、渡された表を正確に覆う行の組です。数独としての保証は、四種類の条件を表へ正しく変換したことに依存します。サンプルでは、復元したすべての盤面を共通検証器へ渡して、この変換も検査しています。

参考文献¶

[1]

Donald E. Knuth. Dancing Links. Millennial Perspectives in Computer Science, pages 187–214, 2000. doi:10.48550/arXiv.cs/0011047.

[2]

Andrzej Kapanowski. Python for Education: The Exact Cover Problem. arXiv preprint arXiv:1010.5890, 2010. doi:10.48550/arXiv.1010.5890.