第4章 miniKanrenで数独を解く¶

空きマスをどの順番で埋めるかは、数独を解く側に委ねられます。16個のマスを未知の変数として用意し、「各行は1から4の並べ替え」「指定マスは初期配置の数字」という条件を並べることで、すべての条件を同時に満たす値の組として完成盤面を定義します。

miniKanren は、このような条件を関係として記述する小さな論理プログラミング言語の一族です。もともとはSchemeの組込み言語として開発され、現在はさまざまな言語へ移植されています [1]。本章ではPythonの kanren 0.3.0 を用います。このライブラリはminiKanrenの設計を基にしており、論理変数、単一化、ゴールの組み合わせと解の列挙機能を提供します [2]。

同じ関係へ違う質問をする¶

数独へ進む前に、二つの列を結合する appendo という関係を試します。 appendo(left, right, whole) は、「left と right をつなげると whole になる」という三項関係です。三つのうち、どれを既知の値にし、どれを未知の値にするかは、問い合わせごとに変えられます。

`appendo` への二つの問い合わせ¶
求めるもの	既知の値	未知の値
結合後の列	`left`、`right`	`whole`
分割位置	`whole`	`left`、`right`

var() と vars() は、問い合わせの途中で値が決まる場所を表す 論理変数 を作ります。これはPythonの変数とは別の役割です。run(個数, 求める値, ゴール) は、ゴールを満たす値を探索します。個数が 1 なら最初の答えを一つ、0 なら見つかる答えをすべて返します。

def append_examples() -> tuple[object, object]:
    whole = var("whole")

    # 左右の列が既知なら、結合後の列を求めます。
    joined = run(1, whole, appendo((1, 2), (3,), whole))

    left, right = vars(2)
    # 結合後の列だけを与えると、同じ関係から分割位置を列挙できます。
    splits = run(0, (left, right), appendo(left, right, (1, 2, 3)))
    return joined, splits

最初の run は、(1, 2) と (3,) をつないだ列を whole に求めます。二つ目は、 (1, 2, 3) を left と right に分ける方法をすべて求めます。実行結果では、同じ appendo から一つの結合結果と四つの分割が得られています。

join: (1, 2, 3)
splits:
  () + (1, 2, 3)
  (1,) + (2, 3)
  (1, 2) + (3,)
  (1, 2, 3) + ()

普通の関数では、入力と返り値の役割が定義によって決まります。appendo が表すのは、一方向の計算ではなく、三つの列が満たす条件です。そのため、結合後の列を求めることも、結合後の列から分割位置を求めることもできます。この使い方を関係プログラミングと呼びます。

ただし、引数の向きを変えれば、どの関係も同じ速さで終了するとは限りません。関係の定義とゴールの順序は、探索の進み方に影響します。 appendo のように複数方向で素直に使える関係は、考え方をつかむための代表例です [3]。

数独でも、初期配置の数字を既知の値、空きマスを論理変数として同じゴールへ渡します。 appendo では列どうしの関係を使いましたが、数独では各行、列、ブロックが1から4の並べ替えになる関係を使います。

単一化で値をそろえる¶

miniKanrenは、二つの項が同じ形になるように論理変数の値をそろえます。この処理を 単一化 と呼びます。たとえば eq(pair, (1, 2)) という条件があり、pair が未知なら、単一化によって pair は (1, 2) になります。二つの項の形や値が両立しなければ、その条件からは答えが生まれません。

単一化を少し形式的に書くと、項 \(t\) と \(u\) に対して、論理変数への代入 \(\sigma\) を探し、次を満たすようにします。

\[\sigma(t) = \sigma(u)\]

ここでの \(\sigma\) は、whole を (1, 2, 3) に対応させる値の対応表です。単一化は二つの項の構造を一致させる操作を指します。

満たしたい条件一つを ゴール と呼びます。eq や appendo の呼び出しはゴールを作り、 run はすべてのゴールを満たす答えを取り出します。ゴールには、条件を同時に満たす組合せと、いずれかを満たせばよい選択肢があります。Pythonの kanren では、選択肢を conde で表せます。

def choice_example() -> tuple[int, ...]:
    number = var("number")
    # condeの各組は選択肢です。ここでは1または2という二つの答えを作ります。
    goal = conde((eq(number, 1),), (eq(number, 2),))
    return run(0, number, goal)

conde に渡す外側の二つの組が「1にする」「2にする」という選択肢です。各組の内側には、その選択肢で同時に満たすゴールを並べます。この例では各選択肢に eq が一つだけあります。

run(0, number, goal) の 0 は、見つかる答えをすべて求める指定です。この例の結果は次のとおりです。

choices: (1, 2)

数独では、一つの完成盤面だけを求めることも、二つ目まで求めて一意性を調べることもできます。

答えをストリームから取り出す¶

一つのゴールが複数の答えを持つとき、miniKanrenは答えの続きを ストリーム として扱います。ストリームは、必要になった分から答えを取り出せる列です。すべての答えを最初にリストへ詰める必要はありません。run(1, ...) なら最初の答え、run(2, ...) なら最初の二つを取り出します。

標準的なminiKanrenの探索では、選択肢のストリームを交互に進めます。一つの選択肢が答えを無限に出し続けても、別の選択肢へ順番が回るようにするためです。この性質は 公平な探索 と呼ばれます。今回使う kanren も、conde の選択肢や複数のゴールから生じる反復子を interleave して答えを作ります [2]。

公平さは、すべての問い合わせが必ず終了するという保証ではありません。ある選択肢が最初の答えも失敗も返さないまま計算を続ければ、ほかへ切り替える地点へ到達できないことがあります。ゴールの書き方や順序が実行に影響する点は残ります。miniKanrenの探索戦略には複数の方式があり、公平さにも段階があることが研究されています [4]。この話は数独コードを読むための前提ではありませんが、run が単純な深さ優先探索と同じではない理由を説明します。

Prologとの違い¶

前章で扱ったPrologも、論理変数と単一化を使って関係を記述します。append/3 を複数方向へ使う構成も同様であり、関係プログラミングのパラダイムはminiKanren固有のものではありません。

違いが見えやすいのは、言語の作りと標準的な探索方法です。Prologは専用の構文、節、述語を備えた言語として使うのが一般的です。miniKanrenは小さな核をPythonやSchemeなどへ埋め込み、ホスト言語のデータや関数と一緒に使います。標準的なProlog処理系は、節とゴールを左から深さ優先で調べます。標準的なminiKanrenは、遅延ストリームを交互に進めます。

どちらにも処理系や拡張があり、探索方法を変更できるため、この比較はすべての実装へ一律には当てはまりません。公式サイトの比較も、両者を言語の一族として扱い、実装ごとの差に注意を促しています [5]。以下では、Pythonへ埋め込んだ関係と run による解の取り出し方に注目します。

4×4数独を関係にする¶

4×4数独には16個のマスがあり、各マスには1から4の数字が入ります。行と列は4本ずつ、 2×2ブロックは4個です。各行、列、ブロックには1から4が一度ずつ現れます。

マスごとに論理変数 \(x_0,\ldots,x_{15}\) を用意します。行、列、ブロックのいずれかを \(U\) とすると、その単位に属する四つの変数へ次の条件を課します。

\[(x_i)_{i\in U} \in \operatorname{Perm}(1,2,3,4)\]

Perm は並べ替えの集合です。各単位が (1, 2, 3, 4) のどれかの並べ替えなら、四つのマスは1から4の範囲に入り、同じ数字も重複しません。初期配置があるマスには \(x_i=d\) という等値関係を追加します。

この章で4×4を使うのは、Pythonの kanren 0.3.0に数独向けの有限領域制約がなく、 permuteq で順列を列挙する実装を選んだからです。並べ替えの個数を表す階乗を使うと、4個の数字には \(4! = 24\) 通りの順列があります。9個では \(9! = 362{,}880\) 通りになり、 27個の単位をこのまま組み合わせるのは不自然に重くなります。9×9へ広げるなら、有限領域制約を備えたminiKanren実装を使うか、数独専用の制約伝播を関係へ加える必要があります。

数独のゴールを作る¶

sudoku_relation は、16個の論理変数と、それらが満たすゴールを返します。行、列、ブロックの位置は共通検証器の units() から取得します。

def sudoku_relation(givens: Board):
    side, _ = board_geometry(givens)
    if side != 4:
        raise ValueError("this example supports 4x4 Sudoku only")

    cells = tuple(vars(len(givens)))
    digits = tuple(range(1, side + 1))
    goals = []

    for cell, given in zip(cells, givens):
        if given:
            # 初期配置を、セルと数字が等しいというゴールにします。
            goals.append((eq, cell, given))

    for unit in units(givens):
        unit_cells = tuple(cells[index] for index in unit)
        # 各行・列・ブロックを1〜4の順列と単一化します。
        goals.append((permuteq, unit_cells, digits))

    return cells, tuple(goals)

(eq, cell, given) や (permuteq, unit_cells, digits) は即時評価される結果ではなく、 kanren の探索過程で展開されるゴール式を表します。探索中に一部の論理変数へ値が割り当てられると、その拘束状態が後続のゴールへ伝播して関係が評価されます。

permuteq(unit_cells, digits) は、二つの列が並べ替えの関係にあることを表します。数独では右側の digits が (1, 2, 3, 4) に固定されているため、左側の各単位へ1から4を一度ずつ割り当てます。行だけを特別扱いする処理はなく、列とブロックにも同じ関係を使います。

解を取り出す¶

solve は作成したゴールを run へ渡します。表示する解の数より一つ多く要求し、まだ別解が残っているかも調べます。

def solve(givens: Board, limit: int = 2) -> Result:
    if limit < 1:
        raise ValueError("limit must be positive")

    cells, goals = sudoku_relation(givens)

    # 表示数より一つ多く要求し、まだ別解が残っているか確かめます。
    found = tuple(tuple(answer) for answer in run(limit + 1, cells, *goals))
    exhausted = len(found) <= limit
    solutions = found[:limit]
    status = "solved" if solutions else "unsat"
    return Result(status, solutions, exhausted)

run が返す答えは、すべてのゴールを満たす16個の値です。共通検証器へ渡せる盤面へ変換し、最大 limit 個を保存します。要求した数に達する前にストリームが枯渇した場合、 exhausted フラグが真となります。このフラグが真の状態で返された答えが1個であれば一意解、 0個であれば解なしと判定します。

実行する¶

サンプルプログラムは examples/03-minikanren/ に実装されています。詳しい実行手順やコマンドラインオプションについては examples/03-minikanren/README.md を参照してください。

一意解の問題¶

最初の問題には四つのヒントがあります。0 は空きマスです。

二つ目までの解を要求しても、一つの解を得た後にストリームが終了するため、一意解であることが確認されます。出力盤面は共通検証器でも確認しています。

解がない問題¶

次の初期配置には、同じ行、列、ブロック内での直接の重複はありません。それでも、すべての単位を1から4の順列にする割り当ては存在しません。

run が解を一つも返さずにストリームが終了するため、解なし（unsat）と判定されます。

解が複数ある問題¶

共通の4×4問題には二つの解があります。

二つの異なる盤面が得られた時点で一意解でないことが分かり、その後にストリームも終了するため、解は全部で二つであることが確認されます。

この方法で分かること¶

各単位を1から4の順列にする関係は、4×4数独の規則を記述しています。有効な完成盤面はすべてのゴールを満たし、ゴールを満たす16個の値の組は有効な完成盤面を構成します。探索空間が有限であるため、ストリームの全域探索により解なしと一意性を判定します。

本実装は順列の直接列挙に依存し、制約伝播や有限領域制約を用いません。本章の4×4数独での検証は、遅延ストリームによる論理探索の動作確認を目的としています。

参考文献¶

[1]

miniKanren Community. miniKanren.org. URL: https://minikanren.org/ (visited on 2026-08-08).

[2] (1,2)

Matthew Rocklin, Lucas Wiman, and contributors. kanren 0.3.0: Logic Programming in Python. 2025. URL: https://pypi.org/project/kanren/0.3.0/ (visited on 2026-08-08).

[3]

William E. Byrd. Relational Programming in miniKanren: Techniques, Applications, and Implementations. PhD thesis, Indiana University, 2009. URL: https://hdl.handle.net/2022/8777.

[4]

Kuang-Chen Lu, Weixi Ma, and Daniel P. Friedman. Towards a miniKanren with Fair Search Strategies. 2019. URL: https://minikanren.org/workshop/2019/minikanren19-final1.pdf (visited on 2026-08-08).

[5]

William E. Byrd. Differences between miniKanren and Prolog. URL: https://minikanren.org/minikanren-and-prolog.html (visited on 2026-08-08).