第5章制約プログラミングで数独を解く¶

ある行に、まだ数字が決まっていないマスが三つあるとします。二つのマスの候補はどちらも {1, 2}、残りのマスは {1, 2, 3} です。この三つには異なる数字を入れなければなりません。最初の二マスは、順序は未定でも1と2を一つずつ使うしかありません。残りのマスから1と2を除けるので、その値は3に決まります。

制約プログラミングでは、各マスが取りうる数字を持ち、「同じ行の値はすべて異なる」といった条件をソルバーへ渡します。ソルバーは条件を使って候補を減らし、それだけで決まらない場合に探索します。先ほどの三マスのように、複数の候補集合をまとめて調べる処理もソルバーが担当します。

この章では、制約モデリング言語 MiniZinc で数独を書き、有限領域制約ソルバー Gecode で解きます。MiniZincモデルはテキストで記述し、コマンドラインから実行します。Pythonは盤面データの受け渡しと、得られた解の検証に使います。

候補を持つ変数と、候補を減らす制約¶

空きマスに最初から一つの数字を入れる代わりに、「1から9のどれか」という未確定の変数を置きます。取りうる値の集合を値域、値域が有限個の値からなる変数を 有限領域変数 と呼びます。MiniZincでは、次の宣言が9×9盤面の81変数を作ります。

この章で使うMiniZincの表記¶
表記	読み方
`var 1..9`	値が未確定の整数変数。値域は1から9
`constraint`	ソルバーが満たすべき条件の宣言
`forall (i in 1..n)`	添字 `i` を動かして同じ制約を繰り返し作る
`[式 \| i in 1..n]`	添字を動かして配列を作る内包表記
`all_different(配列)`	配列の要素がすべて異なる値を取るグローバル制約
`solve satisfy`	最適化ではなく、制約を満たす解を探す指定

array[1..9, 1..9] of var 1..9: cell;

var 1..9 が「値は未確定だが、1から9までの整数に限る」という指定です。通常のプログラムの変数とは違い、宣言した時点で一つの値を代入する必要はありません。最終的な値は、すべての制約を満たすようにソルバーが決めます。[1]

array[1..9, 1..9] は、行と列を1から9で指定する二次元配列です。of var 1..9 が各要素の種類と値域、末尾の cell が配列の名前を表します。

初期配置が5のマスには cell[1, 1] = 5 という制約を加えます。同じ行の別のマスは5を取れなくなり、その変化が列やブロックの制約にも伝わります。制約から値域に入らない値を除き、値域が変わった制約をもう一度調べる処理が 制約伝播 です。どこかの値域が空になれば、その時点の選択からは解を作れないと分かります。

伝播は、必ず一つの値に決める処理ではありません。候補が {2, 5} まで減っても、どちらかを制約だけで除けないことがあります。その場合は一方を選んで制約を追加し、再び伝播します。矛盾したら選択前へ戻って他方を試します。探索の基本形はバックトラックですが、モデルを書く側は、候補の更新や巻き戻しを一手ずつ実装しません。

`all_different` で一行をまとめて表す¶

数独の一行には1から9までの数字が一度ずつ現れます。9個の変数が1から9の値を取り、互いに異なるという一つの制約で表せます。MiniZincの all_different は、配列の要素を互いに異なる値へ制限するグローバル制約です。[2]

行 \(r\) の変数を \(x_{r,1},\ldots,x_{r,9}\) とすれば、意味は次の式でも書けます。

\[\operatorname{all\_different}(x_{r,1},\ldots,x_{r,9}) \quad\Longleftrightarrow\quad \bigwedge_{1 \leq i < j \leq 9} x_{r,i} \ne x_{r,j}\]

右辺は「どの二マスを選んでも値が異なる」という意味です。左辺のように一行を一つの all_different として書くと、ソルバーは行全体の関係として扱えます。

冒頭の {1, 2}、{1, 2}、{1, 2, 3} も同じ例です。最初の二変数が1と2を使い切るため、三つ目から1と2を除けます。このように複数の変数をまとめて表す制約を、グローバル制約と呼びます。

数独をMiniZincで記述する¶

盤面の大きさを \(n\)、ブロック一辺の長さを box とします。9×9なら \(n=9\)、 box = 3 です。givens は入力盤面で、空きマスを0として受け取ります。解を表す cell の値域には0を含めません。

モデル本体は、初期配置、各行、各列、各ブロックの四種類の制約からなります。

% それぞれのマスを、1からnまでの値を取る有限領域変数にします。
array[1..n, 1..n] of var 1..n: cell;

% 初期配置があるマスは、その数字に固定します。
constraint forall (r, c in 1..n where givens[r, c] != 0) (
  cell[r, c] = givens[r, c]
);

% 行と列では、n個のマスがすべて異なる値を取ります。
constraint forall (r in 1..n) (
  all_different([cell[r, c] | c in 1..n])
);
constraint forall (c in 1..n) (
  all_different([cell[r, c] | r in 1..n])
);

% box×boxブロックも、同じall_different制約で表します。
constraint forall (br, bc in 0..box - 1) (
  all_different([
    cell[br * box + dr, bc * box + dc]
    | dr, dc in 1..box
  ])
);

forall は、指定した添字の範囲について同じ制約を作ります。行と列にはそれぞれ9個、ブロックにも9個の all_different が作られるので、合計27個です。各制約には9変数が入り、どのマスも行、列、ブロックの三つの制約に参加します。

角括弧内の 式 | 添字の範囲 は、添字を動かして配列を作るMiniZincの内包表記です。ブロック制約では br と bc がブロックの行と列、dr と dc がブロック内の行と列を表します。たとえば9×9盤面で br = 0、bc = 0 のとき、dr と dc を1から3まで動かして左上の3×3ブロックを取り出します。

このモデルは4×4の数独にも使えます。n = 4、box = 2 とすれば、各変数の値域は1から4、ブロックは2×2になります。数独の規則をループで生成しているため、モデル本体は変わりません。

伝播のあとに探索する¶

伝播だけで盤面が完成しないとき、Gecodeは値が未確定の変数を選び、値域をさらに狭めます。サンプルでは探索方法もMiniZincの注釈で指定します。

% 候補数が最少のマスを選び、残った数字を小さい順に試します。
solve :: int_search(
  [cell[r, c] | r, c in 1..n],
  first_fail,
  indomain_min,
  complete
) satisfy;

int_search の最初の引数は、探索で値を決める cell の一覧です。9×9盤面では81個、 4×4盤面では16個の変数が入ります。末尾の satisfy は、値を最大化または最小化するのではなく、制約を満たす割り当てを探す指定です。 first_fail は、現在の値域が最も小さい変数を先に選びます。たとえば候補が二つのマスを、候補が五つのマスより先に選びます。indomain_min は値域の小さい値から試し、complete は残る選択肢を省略しない探索を指定します。これらの注釈と有限領域探索の動作はMiniZinc Handbookに説明されています。[3]

探索指定は数独の制約そのものではありません。同じモデルであっても探索注釈を省略してGecodeの既定戦略に任せたり、対応する別の戦略に変更したりします。本章では実行結果の再現性を保つため明示的に指定します。

MiniZincとGecodeの役割¶

sudoku.mzn に書いたのは、解が満たす条件と探索の注釈です。MiniZincコンパイラはモデルを、ソルバーが処理しやすい中間形式のFlatZincへ変換します。今回指定したGecodeが、そのFlatZincを受け取って伝播と探索を実行します。Gecodeは整数、真偽値、集合などの制約と探索を扱う制約プログラミング用ツールキットです。 [4]

MiniZincは複数方式のソルバーへ接続できますが、この章の実行結果は --solver gecode を指定したものです。したがって、ここで扱うのはGecodeによる有限領域制約プログラミングです。同じMiniZincモデルをCP-SATソルバーで実行した場合、その内部方式まで同じになるわけではありません。

盤面を直接操作する実装では、候補を減らす関数と探索関数を自分で書きます。ここでは変数の値域と制約を宣言し、制約から値域を狭める伝播と、その後の探索をGecodeに任せます。

実行と検証¶

実行手順とオプションは examples/04-constraint-programming/README.md にまとめています。三つの入力を最大二解まで探索した結果は次のとおりです。

Gecodeで三つの盤面を調べた結果¶
問題	`status`	解数	`search_complete`	`unique`	Gecodeの統計
一意解	`solved`	1	`yes`	`yes`	239ノード、119失敗、5,075伝播
矛盾	`unsat`	0	`yes`	対象外	0ノード、1失敗、43伝播
複数解	`solved`	2	`no`	`no`	3ノード、0失敗、108伝播

一意解問題では、一つ目の解を得た後も探索が続き、二つ目を見つけないまま全探索を終えています。複数解問題の search_complete: no は、指定した二解を得た時点で探索を止めたことを表します。全探索はしていませんが、異なる二盤面が検証を通っているので、一意解でないことは確定します。

ノード数、失敗数、伝播回数はGecode内部の統計です。第1章の探索関数の呼び出し回数とは定義が異なるため、この数値だけで二つの実装の速さは比較できません。

解がない場合と、解が複数ある場合¶

矛盾問題では、初期配置の制約を伝播させた結果、いずれかの変数の値域が空集合となる矛盾状態が発生し、解が存在しない状態（unsat）と判定されます。

複数解問題では、互いに異なる二つの完成盤面が得られた時点で探索を打ち切り、一意解ではない（複数解を持つ）ことが確認できます。

この方法で分かること¶

有限領域の全域探索を指定するため、解が存在する場合は完成盤面を出力します。全探索を終了して解が存在しない場合は unsat となります。最大二解の探索により、一解のみで全域探索が終了した場合は一意解、二解が得られた場合は複数解と確定します。

乱数を用いない決定論的な実行であるため、同一の処理系、モデル、入力、探索指定であれば解の出力順序と統計値を再現します。MiniZincやGecodeのバージョン、ソルバー、探索注釈を変更した場合は、探索順序や統計値が変化することがあります。

数独の規則は27個の all_different 制約として定式化されます。条件を追加することで、対角線上の数字も異なる対角線数独や、不等号条件を持つ数独へ拡張します。制約伝播のみで決まらない盤面では探索を要し、問題構造に応じて探索量が増加する点は、第1章でバックトラックを直接実装した場合と同様です。

参考文献¶

[1]

MiniZinc Team. The MiniZinc Handbook. URL: https://docs.minizinc.dev/en/stable/ (visited on 2026-08-08).

[2]

MiniZinc Team. All-Different and Related Constraints. URL: https://docs.minizinc.dev/en/stable/lib-globals-alldifferent.html (visited on 2026-08-08).

[3]

MiniZinc Team. Search. URL: https://docs.minizinc.dev/en/stable/mzn_search.html (visited on 2026-08-08).

[4]

Gecode Team. Gecode Documentation. URL: https://www.gecode.dev/documentation.html (visited on 2026-08-08).

第5章 制約プログラミングで数独を解く¶