第19章

素朴な数独ソルバー

（やさしい版） Pearls of Functional Algorithm Design（関数プログラミングによるアルゴリズム設計の真珠）

どんな話？

この章は、みんなが知っている 数独 を解く Haskell プログラムを、簡単な仕様から出発して、式を書きかえる（等式的推論）だけでだんだん速い版に変えていく、という話です。

この章のゴール 数独盤を「9 × 9 の文字の行列」として扱い、次の 3 つのステップで解く関数 solve を作ります。

はじめに

数独ってなに？

数独は 9 × 9 のマス目のゲームです。図 19.1 のような盤が与えられたとき、空きマスに 1〜9 の数字を入れて、次の 3 つを守るように埋めます。

ちゃんと作られた数独パズルなら、答えは必ず 1 通りです。ここではまず「全部の埋め方」を返す関数 solve を作ります。1 個だけ欲しいときは、そのリストの先頭を取ればよい。Haskell は遅延評価なので、その場合は最初の 1 個しか実際には計算されません。

457
94
368
726
42
893
456
53
619
図 19.1   数独の盤面

仕様（まずはバカ正直な版）

データ型：盤とは何か

まず「行列」を型として書きます。

type Matrix a = [Row a] type Row a = [a]
Dart // 行列 = 行のリスト。行は要素のリスト。 typedef Row<A> = List<A>; typedef Matrix<A> = List<Row<A>>;

m × n の行列とは、長さ n の行が m 本並んだリストです。数独の盤面（Grid）は 9 × 9 の文字の行列。

type Grid = Matrix Digit type Digit = Char
Dart // 数字は 1 文字（'0' が空きマス）。盤面は 9×9 の文字行列。 typedef Digit = String; typedef Grid = Matrix<Digit>;

使う「数字」は 1〜9 の文字。空きマスは '0' で表すことにします。

digits = ['1' .. '9'] blank = (== '0')
Dart const List<Digit> digits = ['1','2','3','4','5','6','7','8','9']; bool blank(Digit d) => d == '0';
前提 入力の盤面には数字と '0'（空き）しか出てこないとし、しかも「行・列・ブロックに同じ数字が重複していない」正しい盤面だとします。

3段構えのシンプルな仕様

いちばん単純に書くと、こうなります。

solve = filter valid · expand · choices

読み方はこう。

関数の型はこうです。

choices :: Grid → Matrix Choices expand :: Matrix Choices → [Grid] valid :: Grid → Bool

choices ― 各マスに候補を入れる

候補型を単純に type Choices = [Digit] とすれば、こう書けます。

choices :: Grid → Matrix Choices choices = map (map choice) choice d = if blank d then digits else [d]
Dart // 候補型 = 数字のリスト。 typedef Choices = List<Digit>; Choices choice(Digit d) => blank(d) ? List.of(digits) : [d]; Matrix<Choices> choices(Grid g) => [for (final row in g) [for (final d in row) choice(d)]];

「空きなら全部の数字を候補にする、そうでなければ確定なのでリストの中身は 1 個だけ」というだけの話です。

expand ― 候補を全部組み合わせる

expand は「行列の各マスに入るリストを、あらゆる組み合わせで一つずつ選ぶ」ということ。まさに行列のデカルト積です。

expand :: Matrix Choices → [Grid] expand = cp · map cp
Dart // 各行をデカルト積で展開してから、行方向にもデカルト積を取る。 List<Grid> expand(Matrix<Choices> m) => cp<Row<Digit>>([for (final row in m) cp<Digit>(row)]);

ここで cp（Cartesian product）はリストのリストのデカルト積を返します。

cp :: [[a]] → [[a]] cp [] = [[]] cp (xs : xss) = [x : ys | x ← xs, ys ← cp xss]
Dart // リストのリストのデカルト積。 List<List<A>> cp<A>(List<List<A>> xss) { if (xss.isEmpty) return [[]]; final xs = xss.first; final rest = cp<A>(xss.sublist(1)); return [for (final x in xs) for (final ys in rest) [x, ...ys]]; }
具体例 cp [[1, 2], [3], [4, 5]] = [[1, 3, 4], [1, 3, 5], [2, 3, 4], [2, 3, 5]]。
つまり map cp で「各行の全パターン」を作り、外側の cp でそれを行方向に全部組み合わせているだけ。

valid ― 正しい盤面かチェック

正しい盤面 = どの行にも列にもブロックにも重複がない、ということ。

valid :: Grid → Bool valid g = all nodups (rows g) ∧ all nodups (cols g) ∧ all nodups (boxs g)
Dart bool valid(Grid g) => rows(g).every(nodups) && cols(g).every(nodups) && boxs(g).every(nodups);

nodups（重複なし判定）は素直に書けます。

nodups :: Eq a ⇒ [a] → Bool nodups [] = True nodups (x : xs) = all (≠ x) xs ∧ nodups xs
Dart // 重複なし判定（素直な n^2 版）。 bool nodups<A>(List<A> xs) { for (var i = 0; i < xs.length; i++) { for (var j = i + 1; j < xs.length; j++) { if (xs[i] == xs[j]) return false; } } return true; }
ちょっとした余談 nodups は二乗時間（n2）。ソート（n log n）を使うことも考えられるけれど、n = 9 では効くとは限らない。「2·92 = 162 ステップ」と「100·9·log2 9 ≈ 2853 ステップ」、どっちが速い？（そう、素直な nodups のほうが小さな n では速いのです。）

rows / cols / boxs ― 行・列・ブロックの取り出し方

行列を「行のリスト」で持っているので、rows は何もしない恒等関数。

rows :: Matrix a → Matrix a rows = id
Dart Matrix<A> rows<A>(Matrix<A> m) => m;

cols は転置（行と列を入れ替える）。

cols :: Matrix a → Matrix a cols [xs] = [[x] | x ← xs] cols (xs : xss) = zipWith (:) xs (cols xss)
Dart // 行列の転置（行と列を入れ替える）。 Matrix<A> cols<A>(Matrix<A> m) { if (m.length == 1) return [for (final x in m.first) [x]]; final xs = m.first; final rest = cols<A>(m.sublist(1)); return [for (var i = 0; i < xs.length; i++) [xs[i], ...rest[i]]]; }

boxs はもう少し面白い。行列を「3 個ずつのブロックの並び」として作りかえる操作を、group・ungroup・cols を組み合わせて表現します。

boxs :: Matrix a → Matrix a boxs = map ungroup · ungroup · map cols · group · map group
Dart // map ungroup · ungroup · map cols · group · map group Matrix<A> boxs<A>(Matrix<A> m) { final step1 = [for (final row in m) group<A>(row)]; // 各行を 3 個ずつに final step2 = group<List<A>>(step1); // 行方向にも 3 本ずつ final step3 = [for (final block in step2) cols<List<A>>(block)]; final step4 = ungroup<List<A>>(step3); return [for (final row in step4) ungroup<A>(row)]; }
group :: [a] → [[a]] group [] = [] group xs = take 3 xs : group (drop 3 xs) ungroup :: [[a]] → [a] ungroup = concat
Dart List<List<A>> group<A>(List<A> xs) { final out = <List<A>>[]; for (var i = 0; i < xs.length; i += 3) { out.add(xs.sublist(i, i + 3 > xs.length ? xs.length : i + 3)); } return out; } List<A> ungroup<A>(List<List<A>> xss) => [for (final xs in xss) ...xs];

4 × 4 盤（2 個ずつグループ化）で動きを見るとこんな感じ。

(a b c d / e f g h / i j k l / m n o p) → ((ab cd)(ef gh) / (ij kl)(mn op)) → ((ab ef)(cd gh) / (ij mn)(kl op))

大事な性質：3 つの関数はどれも「対合」

添字を使ってちまちま計算するのではなく、行列を「まとまり」として扱っているのがミソです。この流儀を wholemeal programming（丸ごとプログラミング）と呼びます。添字で書くと「添字病（indexitis）」にかかりがちですが、丸ごと書けば法則を使った書きかえがしやすくなります。

実際、N2 × N2 行列で次の 3 つの法則が成り立ちます。

rows · rows = id cols · cols = id boxs · boxs = id
ポイント この 3 つは「2 回やると元に戻る」ということ（対合）。とくに cols（転置の対合性）は、証明してみると案外難しい。boxs の対合性は、cols の対合性と group · ungroup = id を使えば計算で導けます。

さらに、選択肢の行列については次の 3 つの法則も成り立ちます。

map rows · expand = expand · rows (19.1) map cols · expand = expand · cols (19.2) map boxs · expand = expand · boxs (19.3)

この 3 つは、あとの計算で使います。

選択肢を減らそう ― 枝刈り（prune）

なぜ素朴な仕様ではダメか

理屈のうえでは動きますが、実際には手も足も出ません。81 マスのうち半分くらいがはじめから確定していると甘めに見積もっても、残りの候補の総数はおよそ 940、つまり

147 808 829 414 345 923 316 083 210 206 383 297 601

通りの盤面をチェックしなきゃならないからです。桁が違いすぎ。

アイデア：確定した数字を候補から取り除く

「あるマス c と同じ行・列・ブロックに、すでに確定している数字（候補が 1 個しかないマス）がある。その数字は c の候補からは除いてしまえる」――これが枝刈りの発想です。次の prune を作りたい。

prune :: Matrix Choices → Matrix Choices

これが

filter valid · expand = filter valid · expand · prune

を満たすなら、途中で候補を減らしても結果は変わりません。

まずは 1 行だけ枝刈り

行列は行のリストなので、まず 1 行だけ枝刈りする関数から作ります。

pruneRow :: Row Choices → Row Choices pruneRow row = map (remove fixed) row where fixed = [d | [d] ← row] remove xs ds = if singleton ds then ds else ds \\ xs
Dart // 1 行から確定数字を集め、他マスの候補から取り除く。 Row<Choices> pruneRow(Row<Choices> row) { final fixed = [for (final ds in row) if (ds.length == 1) ds[0]]; Choices remove(Choices ds) => ds.length == 1 ? ds : [for (final d in ds) if (!fixed.contains(d)) d]; return [for (final ds in row) remove(ds)]; }

fixed はその行の「確定している数字」の集まり。remove は、まだ確定していないマスの候補から fixed の数字を消します（確定しているマスはそのまま）。

この pruneRow は次の性質を満たします。

filter nodups · cp = filter nodups · cp · pruneRow (19.4)

（証明は演習）

filter に関する 2 つの補題

prune 全体を導くには filter の 2 つの法則が要ります。まず f · f = id なら

filter (p · f) = map f · filter p · map f (19.5)

もうひとつは

filter (all p) · cp = cp · map (filter p) (19.6)

（どちらも証明は演習）

計算：boxs の場合

出発点は次の分解です。

filter valid · expand = filter (all nodups · boxs) · filter (all nodups · cols) · filter (all nodups · rows) · expand

順序は問わないので、それぞれの filter を expand と組み合わせて変形します。boxs の場合はこう。

filter (all nodups · boxs) · expand = {(19.5)、boxs · boxs = id より} map boxs · filter (all nodups) · map boxs · expand = {(19.3)} map boxs · filter (all nodups) · expand · boxs = {expand の定義} map boxs · filter (all nodups) · cp · map cp · boxs = {(19.6) と map f · map g = map (f · g)} map boxs · cp · map (filter nodups · cp) · boxs = {(19.4)} map boxs · cp · map (filter nodups · cp · pruneRow) · boxs = {(19.6)} map boxs · filter (all nodups) · cp · map cp · map pruneRow · boxs = {expand の定義} map boxs · filter (all nodups) · expand · map pruneRow · boxs = {(19.5) を map f · filter p = filter (p · f) · map f で} filter (all nodups · boxs) · map boxs · expand · map pruneRow · boxs = {(19.3)} filter (all nodups · boxs) · expand · boxs · map pruneRow · boxs

結果、次のことが言えました。

filter (all nodups · boxs) · expand = filter (all nodups · boxs) · expand · pruneBy boxs

ここで pruneBy f = f · map pruneRow · f と置きました。rows・cols についても同じ計算をすれば

filter valid · expand = filter valid · expand · prune

で、

prune = pruneBy boxs · pruneBy cols · pruneBy rows
Dart // f は対合（f · f = id）。行方向に pruneRow を掛けて元に戻す。 Matrix<Choices> pruneBy( Matrix<Choices> Function(Matrix<Choices>) f, Matrix<Choices> m) { final t = f(m); final pruned = [for (final row in t) pruneRow(row)]; return f(pruned); } Matrix<Choices> prune(Matrix<Choices> m) => pruneBy(boxs, pruneBy(cols, pruneBy(rows, m)));

となります。まとめて solve の新版はこう。

solve = filter valid · expand · prune · choices
Dart // 第 2 版：choices → prune → expand → filter valid。 // 枝刈りしても expand の爆発は残るので、実用性はほぼない。 List<Grid> solveV2(Grid g) => expand(prune(choices(g))).where(valid).toList();
ポイント prune は 1 回でも何回でも挟んで OK。1 回枝刈りしたあとに新しく確定するマスが増えて、もう 1 回枝刈りするとさらに候補が減る、ということが起こるからです。やさしめの数独なら、この繰り返しだけで解けてしまいます。

1 マスずつ広げる ― 単一マス展開

アイデア

枝刈りだけでは進まなくなる、意地悪なパズルもあります。そこでもう 1 手：候補が一番少ないマスを 1 個だけ選び、そのマスの候補を場合分けする。他のマスの候補はいじりません。展開したそれぞれの盤面にまた prune をかけて…と繰り返します。

expand1 の性質

そういう関数 expand1 を作ります。答えの並び順を除けば

expand = concat · map expand · expand1 (19.7)

を満たしてほしい。展開のターゲットは「候補が 1 でない中で、いちばん候補数が少ないマス」にすると効率がいい。候補が 0 のマスがあれば「もう解けない」と早く分かるので、そういう発見にもつながります。

候補 cs のマスが row の途中にあり、row = row1 ++ [cs] ++ row2、行列は rows1 と rows2 に上下に分かれる、と表せば次のように書けます。

expand1 :: Matrix Choices → [Matrix Choices] expand1 rows = [rows1 ++ [row1 ++ [c] : row2] ++ rows2 | c ← cs] where (rows1, row : rows2) = break (any smallest) rows (row1, cs : row2) = break smallest row smallest cs = length cs == n n = minimum (counts rows) counts = filter (≠ 1) · map length · concat
Dart // 候補が最小のマス（サイズ > 1）を 1 つ選び、その候補ごとに展開。 List<Matrix<Choices>> expand1(Matrix<Choices> rowsM) { // counts：候補数が 1 でないマスの候補数一覧 final counts = [ for (final row in rowsM) for (final ds in row) if (ds.length != 1) ds.length ]; final n = counts.reduce((a, b) => a < b ? a : b); bool smallest(Choices cs) => cs.length == n; // 該当マスを含む最初の行を探す final r = rowsM.indexWhere((row) => row.any(smallest)); final rows1 = rowsM.sublist(0, r); final row = rowsM[r]; final rows2 = rowsM.sublist(r + 1); final c = row.indexWhere(smallest); final row1 = row.sublist(0, c); final cs = row[c]; final row2 = row.sublist(c + 1); return [ for (final d in cs) [ ...rows1, [...row1, [d], ...row2], ...rows2, ] ]; }

n は「候補が 1 でないマスの中での最小候補数」。break p はリストを「p を満たさない部分」と「そこから先」に分けます。

break p xs = (takeWhile (not · p) xs, dropWhile (not · p) xs)
Dart // リストを p が最初に真になる直前で 2 つに分ける。 (List<A>, List<A>) breakAt<A>(bool Function(A) p, List<A> xs) { final i = xs.indexWhere(p); return i < 0 ? (xs, <A>[]) : (xs.sublist(0, i), xs.sublist(i)); }
動きを言葉で
  1. break (any smallest) rows：「最小候補のマスを含む最初の行」までで行を切り、その行を row にする。
  2. break smallest row：その行の中でも、最小候補のマス cs のところで切る。
  3. cs の各候補 c について、そのマスを [c]（確定）に置き換えた行列を作り、リストで返す。
  4. もし候補が 0 個なら、結果は空リスト。

「完成した／不安全」の判定

n の定義から、(19.7) は「単一要素でないマスが 1 個以上ある行列」に対してだけ成り立ちます。そこで用語を決めておきます。

complete = all (all single) safe m = all ok (rows m) ∧ all ok (cols m) ∧ all ok (boxs m) where ok row = nodups [d | [d] ← row]
Dart bool complete(Matrix<Choices> m) => m.every((row) => row.every((ds) => ds.length == 1)); bool _ok(Row<Choices> row) => nodups([for (final ds in row) if (ds.length == 1) ds[0]]); bool safe(Matrix<Choices> m) => rows(m).every(_ok) && cols(m).every(_ok) && boxs(m).every(_ok);

最終形の solve

「安全だが未完成な行列」に対して次のように計算できます。

filter valid · expand = {未完成な行列上では expand = concat · map expand · expand1} filter valid · concat · map expand · expand1 = {filter p · concat = concat · map (filter p)} concat · map (filter valid · expand) · expand1 = {filter valid · expand = filter valid · expand · prune} concat · map(filter valid · expand · prune) · expand1

search = filter valid · expand · prune と置けば、安全かつ未完成な行列上で

search · prune = concat · map search · expand1

これで solve の第 3 版が書けます。

solve = search · choices search m | not (safe m) = [] | complete m' = [map (map head) m'] | otherwise = concat (map search (expand1 m')) | where m' = prune m
Dart // 最終版：prune で枝刈り → 完成なら答え → そうでなければ 1 マス展開して再帰。 List<Grid> search(Matrix<Choices> m) { if (!safe(m)) return const []; final mp = prune(m); if (complete(mp)) { return [ [for (final row in mp) [for (final ds in row) ds.first]] ]; } return [for (final m2 in expand1(mp)) ...search(m2)]; } List<Grid> solve(Grid g) => search(choices(g));
読み方 各盤面 m に対して、 これが最終版の素朴な数独ソルバーです。

終わりに

速度の実測

実測結果

まとめ

Haskell Wiki には 10 個以上の数独ソルバーがあり、いずれも座標計算・配列・モナドをうまく使っています。SAT ソルバーや制約充足に落とすものもあります。それでもここで作ったものは、たぶん最も単純で最も短い部類のひとつです。しかも、そのかなりの部分が式の書きかえ（等式的推論）だけで導かれた――これが本章のいちばんの見どころです。

Dart // 章末：solve を動かしてみる。'0' が空きマス。 void main() { final puzzle = <String>[ '004005700', '000000940', '360000008', '720060000', '000402000', '000080093', '400000056', '005300000', '006100900', ]; final grid = [for (final line in puzzle) line.split('')]; final answers = solve(grid); print('解の個数: ${answers.length}'); for (final row in answers.first) { print(row.join('')); } // 解の個数: 1 // 894325761 …（1 通りの完成盤が表示される） }