第6章 Answer Set Programmingで数独を解く

数独の完成盤面を、value(4,7,2) のような事実81個の集まりとして表してみます。この例は 「4行7列の値は2」を意味します。各マスについて数字を一つ選び、行、列、3×3ブロックの重複を 含む集まりを除けば、残ったものが完成盤面です。

Answer Set Programming（ASP） は、 候補を作る規則と、認めない組合せを表す規則をまとめて記述し、条件に合う安定モデル （answer set）を求める方法です。この章では clingo 5.8.0を 使います。

選択肢から安定モデルを作る

最初に、tea、coffee、waterから飲み物を一つ選ぶ小さな例を見ます。

drink(tea) のように、対象とその関係を記号で表したものを 原子 と呼びます。この章の 例では、プログラム全体の規則に認められる原子の集合が一つの安定モデルです。たとえば drink(tea) だけを選んだ集合と、drink(water) だけを選んだ集合は別の安定モデルです。

この章で使うASPの表記

表記

読み方

name(args).

末尾の . は規則や事実の終わり

a :- b, c.

b と c が成り立てば a も成り立つ（規則）

:- condition.

condition が成り立つ候補を認めない（整合性制約）

L { head : cond } U

条件を満たす head から L 個以上 U 個以下を選ぶ（choice rule）

#show name/N.

出力に name/N だけを表示する指定

 
% 選べる飲み物を事実として並べます。
option(tea; coffee; water).

% 三つの候補から、ちょうど一つを選びます。
1 { drink(X) : option(X) } 1.

% coffeeを含む候補は、安定モデルとして認めません。
:- drink(coffee).

#show drink/1.

option(tea; coffee; water). は三つの事実をまとめて書いたものです。次の行は choice rule です。option/1 や drink/1 の /1 は、述語が引数を一つ取ることを表します。大文字で 始まる X はclingoが具体的な値へ展開する変数で、Pythonの変数ではありません。

1 { drink(X) : option(X) } 1.

波括弧内の drink(X) から、一つ以上かつ一つ以下、すなわちちょうど一つを選びます。 : の右側は選択肢になる条件で、X には option/1 のtea、coffee、waterが入ります。 波括弧の左右にある 1 は、選ぶ個数の下限と上限です。

:- drink(coffee). は 整合性制約 です。:- の右側が成り立つ候補を認めません。この 例ではcoffeeを選んだ候補が除かれます。最後の #show drink/1. は、安定モデルのうち drink/1 だけを出力する指定です。choice ruleや整合性制約を含む入力形式はASP-Core-2として 標準化されています [1]。

$ UV_CACHE_DIR=.uv-cache uv run \
    --with-requirements examples/09-asp/requirements.txt \
    python examples/09-asp/choice.py

clingo: 5.8.0
models: 2
answer 1: drink(tea)
answer 2: drink(water)

出力された drink(tea) と drink(water) が、それぞれ一つの安定モデルです。実際の モデルには option/1 の事実も含まれますが、#show によって表示を選択結果だけに 絞っています。choice ruleはまずtea、coffee、waterを選ぶ三候補を作ります。整合性制約が drink(coffee) を含む候補を除くため、二つのモデルが残ります。

補足

安定モデルは、プログラム全体の規則から認められる原子の集合です。規則に根拠のない原子を 自由に足した集合まで答えにはしません。この小例と後の数独プログラムには、否定を介した 再帰がありません。そのため「choice ruleで割当を作り、整合性制約を破る割当を除く」構造を 持ちます。

Prologの問い合わせとの違い

第3章「Prolog」では、たとえば blocked_in_row(1, Col, 5) と問い合わせ、条件を満たす Col の束縛を 順に受け取ります。呼び出したゴールから規則をたどり、別の答えはバックトラックで求めます。

ASP例では、drink(X) を問い合わせとして呼び出しません。事実、choice rule、整合性制約を 含むプログラム全体をclingoへ渡します。clingoが返すものは変数 X の束縛ではなく、同時に 成り立つ原子の集合です。数独なら、一つの安定モデルに完成盤面の81個の value/3 が入ります。

この違いは、探索順を書く場所にも現れます。ASPプログラムには「最初の空きマスを選び、失敗したら 戻る」という手順を書きません。規則の並び順に沿ってゴールを実行する説明も必要ありません。 clingo内部では探索が行われますが、原稿のコードが記述するのは、完成盤面として認める原子の 組合せです。

数独の候補と禁止条件を書く

数独のASPプログラムでは、行、列、数字を1から9までの事実として用意します。各マスの数字は、 次のchoice ruleで一つだけ選びます。

1 { value(R, C, D) : digit(D) } 1 :- row(R), column(C).

R と C が表す81マスのそれぞれについて、D を一つ選ぶ規則です。残りの規則は、 数独に反する選択を整合性制約で除きます。

row(1..9).
column(1..9).
digit(1..9).

% 各マスについて、数字をちょうど一つ選びます。
1 { value(R, C, D) : digit(D) } 1 :- row(R), column(C).

% 同じ行や列で、同じ数字を二度使う割当を除きます。
:- value(R, C1, D), value(R, C2, D), C1 < C2.
:- value(R1, C, D), value(R2, C, D), R1 < R2.

% 行と列から3×3ブロックの番号を計算します。
block(R, C, B) :-
    row(R), column(C),
    B = ((R - 1) / 3) * 3 + ((C - 1) / 3) + 1.

% 同じブロックで、同じ数字を二度使う割当を除きます。
:- value(R1, C1, D), value(R2, C2, D),
   block(R1, C1, B), block(R2, C2, B),
   P1 = (R1 - 1) * 9 + C1, P2 = (R2 - 1) * 9 + C2, P1 < P2.

% 初期配置と異なる数字を選んだ割当を除きます。
:- given(R, C, D), not value(R, C, D).

#show value/3.

行の制約では、同じ行と数字を持つ二つの value があり、列番号が異なる候補を除きます。 C1 < C2 は同じ二マスを逆順でも調べないための条件です。列についても同じ形です。

block/3 は、行と列から1〜9のブロック番号を計算します。/ はここでは整数除算です。 ブロックの制約は、同じ数字を持つ二つの value が同じブロックに属する候補を除きます。 P1 と P2 は、行と列を1から81の位置番号へ変換した値です。P1 < P2 を加えることで、 同じ二マスを逆順にもう一度調べることを避けています。

初期配置はPython側から given(行,列,数字). という事実として加えます。最後の整合性制約は、 given/3 があるのに対応する value/3 が選ばれていない候補を除きます。ASPの not は 「その原子を導けない」というデフォルト否定です。このプログラムでは、初期配置と異なる完成盤面を 拒否するためにだけ使っています。

groundしてからsolveする

ソース中の R、C、D は変数ですが、clingoのsolverが直接この変数を割り当てるわけでは ありません。最初にgrounderが row(1..9) などの有限範囲を使い、変数を具体的な数字へ 展開します。たとえば R=1, C=1 については、value(1,1,1) から value(1,1,9) までの 九候補から一つを選ぶ規則になります。マスごとのchoice ruleは、このような基礎化された規則81個へ 展開されます。

groundingで得た変数のないプログラムを、solverが探索します。clingoはgrounderとsolverを統合した 処理系で、Python APIから二段階を明示的に呼び出せます。Potasscoの処理系とASPによる宣言的な 問題記述については、開発チームの解説もあります [2]。

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

    control = clingo.Control(["--warn=none"])
    control.configuration.solve.models = limit
    control.load(str(PROGRAM))
    # 初期配置をgiven/3の事実として、数独の規則と同じprogram partへ加える。
    control.add("base", [], given_facts(board))

    # 変数を具体的な定数へ展開してから、安定モデルを探索する。
    control.ground([("base", [])])
    solutions: list[Board] = []
    with control.solve(yield_=True) as handle:
        for model in handle:
            solutions.append(board_from_model(model))
        result = handle.get()

    status = "solved" if solutions else "unsat" if result.unsatisfiable else "unknown"
    return AspResult(status, tuple(solutions), result.exhausted)

control.add() は初期配置を数独規則と同じ base 部へ加えます。ground() が規則を 基礎化し、solve(yield_=True) が安定モデルを順に返します。#show value/3 があるため、 model.symbols(shown=True) から盤面に必要な原子だけを取り出せます。clingoのガイドにも、 choice rule、整合性制約、groundingとsolveの例が掲載されています [3]。

実行と検証

モデルの実行および検証手順については examples/09-asp/README.md を参照してください。

通常問題では安定モデルがちょうど一つ見つかり、二つ目を検索しても全探索空間の走査が完了（exhausted: yes）することから一意解であることが判定できます。

解がない問題

矛盾問題では、すべての規則と整合性制約を同時に満たす安定モデルが存在しません。探索を完了した結果、安定モデル数が0となるため解なし（unsat）と判定されます。

解が複数ある問題

複数解問題では、二つの異なる安定モデルが得られた時点で指定した上限に達し、探索を打ち切ります。 全探索は完了していませんが、この時点で一意解ではない（複数解を持つ）ことが判定されます。

この方法で分かること

この数独プログラムでは、規則を満たす完成盤面と、value/3 を表示した安定モデルが一対一に 対応します。clingoが全モデルの探索を終えれば、0モデルから解なしを、一モデルから一意解を 判定します。二モデルが得られた時点で複数解と決定します。

SolveResult.exhausted を確認しているため、モデル数の上限に達した場合と、全探索を終えた場合を 区別しています。実行時間の上限や割り込みは設定していません。掲載コードで unknown が 返るのは、solverが充足可能性を決定できないまま終了した場合です。

モデルの列挙順はASPプログラムの意味に含まれません。サンプルは乱数オプションを使っていませんが、 clingoの版や探索設定が変われば、複数解のどちらを先に返すかは変化します。一意性の判定には、 モデルの順序ではなく個数と exhausted を使います。

ASPソルバーが保証するのは、渡したプログラムの安定モデルです。数独としての保証は、choice ruleと 整合性制約が数独の規則を正しく表していることに依存します。サンプルでは、復元した全盤面を 共通検証器へ渡して変換も検査しています。

参考文献

[1]

Francesco Calimeri, Wolfgang Faber, Martin Gebser, Giovambattista Ianni, Roland Kaminski, Thomas Krennwallner, Nicola Leone, Marco Maratea, Francesco Ricca, and Torsten Schaub. ASP-Core-2 Input Language Format. Theory and Practice of Logic Programming, 20(2):294–309, 2020. doi:10.1017/S1471068419000450.

[2]

Martin Gebser, Benjamin Kaufmann, Roland Kaminski, Max Ostrowski, Torsten Schaub, and Marius Schneider. Potassco: The Potsdam Answer Set Solving Collection. AI Communications, 24(2):107–124, 2011. doi:10.3233/AIC-2011-0491.

[3]

Potassco Team. The Potassco Guide. 2026. URL: https://potassco.org/guide/ (visited on 2026-08-08).