Thinking Functionally with Haskell勉強メモ: 第５章３ 不確定なマスを再帰的に「みなし確定」させて枝刈り

前回のsolveは「すでに確定したマスの値を使って枝刈り」の後に「残った各マスの取り得る値の全探索」という解決方法だった。

これでも相当な効率化が図られているが、「残った各マスの取り得る値の全探索」のほうにまだまだ改善の余地が残されている。例えば４つのマスがひとつの行に未確定で残されている場合、全探索だと調べる組み合わせの総数はだが、実際にはで探索できる。

一つの未確定のマスを「確定した」とみなしてできるMatrix [Digit]を、そのマスが取り得る値の分だけ作成して[Matrix [Digit]]リストにする。そこにmap pruneを適用して、さらに残った未確定のマスを・・・　と再帰的にやっていけばいい。

そのための関数が：

expand1 :: Matrix [Digit] -> [Matrix [Digit]]

以下の等式が成り立つ：

expand = concat . map expand . expand 1

再帰的にexpandを展開していけることがわかる。

Solve関数

まずは最終的に定義するSolveを見せる：

solve = search . choices

search :: Matrix [Digit] -> [Matrix [Digit]]
search choiceMatrix
  | not (safe prunedMatrix) = []
  | complete prunedMatrix = [extract prunedMatrix]
  | otherwise      =  concat (map search (expand1 prunedMatrix))
  where prunedMatrix = prune choiceMatrix

choicesとpruneは前回と同じ定義。

以下、パターンマッチの行を個別に見ていく。

| not (safe prunedMatrix) = []

safeとはあるMatrix [Digits]の確定したマスが、行・列・箱でダブっていないか確認するもの：

safe :: Matrix [Digit] -> Bool
same m = all ok (rows cm) &&
         all ok (cols cm) &&
         all ok (cols cm)
ok row = nodups [x | [x] <- row]

この定義はvalidの定義に似ている：

valid g = all nodups (rows g) &&
          all nodups (cols g) &&
          all nodups (boxs g)

ただし、valid ::Matrix Digit -> Boolなので扱う型が違う。

We can also usefully generalize valid to test on matrices of choices

と書いてあるが、これはgeneralizeではないよな？と思ってしまうがどうなのだろう。

| not (safe prunedMatrix) = []

の意味は、もしpruneによって確定したマスに数独のルール違反のダブりが確認された場合は空リストを返す、というもの。

| complete prunedMatrix = [extract prunedMatrix]

まずはcompleteの定義：

complete :: Matrix [Digit] -> Bool
complete :: all (all single)

single :: [a] -> Bool
single [_] = True
single _ = False

singleはあるリストが要素数１かどうかを調べる関数。Don't Careパターンマッチがなかなかかっこいい。

completeはあるMatrix [Digit]の[Digit]部分がすべて要素数１か、つまりそのMatrixはすべての値が確定しているかどうかを確認する関数。

つぎにextract：

extract :: Matrix [Digit] -> Matrix Digit
extract = map (map head)

Matrix [Digit]のすべての[Digit]要素から、そのリストの最初の要素を摘出してMatrix Digitを返す関数。

つまり| complete prunedMatrix = [extract prunedMatrix]は、すべてのマスが確定しているなら、その確定した値のMatrixだけをリストを返す。

| otherwise = concat (map search (expand1 prunedMatrix))

この部分が一番のキモで、前述のexpand1してから再帰的にsearchをmapしている。

expand1の定義：

expand1 :: Matrix [Digit] -> [Matrix [Digit]]
expand1 matrix
  = [rows 1 ++ [cells1 ++ [[c]] ++ cells2] ++ rows2 | c <- cs]
   where
   (rows1, row:rows2) = break (any smallest) matrix
   (cells1, cs:cells2) = break smallest row
   smallest cs = length cs == n
   n = minimum (counts matrix)

counts :: Matrix [Digit] -> [Int]
counts = filter (/= 1) . map length . concat)

break :: (a -> Bool) -> [a] -> ([a], [a])
break p = span (not . p)

any :: (a -> Bool) -> [a] -> Bool
any p = or . map p

あるマスが取り得る値をそのマスの自由度と呼ぼう。全未確定（自由度!=1）マスの中で自由度が最低のものを選んで、それをベースに探索している。

自由度が0のマスが存在する場合はexpand1は空リストを返すので、数独ルールに反したMatrix内容になったらすぐ探索が打ち切られるようになっている。

ちなみにこのexpand1関数、すでにすべてのマスが確定しているMatrixが引数だとany smallestが空リストを返し、break (any smallest) matrixがエラーになるので気をつけなければいけない。searchでは先に| complete choiceMatrix = ...のマッチでそのケースを排除している。

証明

というわけでsolve関数の各部分を解説してきた。あとはこれが以前のsolveと等価であることを証明する。

まず、引数がunsafeな場合、filter valid . expandは空リストを返す：

filter valid . expand = []

引数がsafeでcompleteな場合：

filter valid . expand m = [extract m]

最後に、引数がsafeでcompleteな場合：

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) . map expand . expand1

= {functor law of map}
concat . map (filter valid . expand) . expand1

filter valid . expand = concat . map (filter valid . expand) . expand1

search = filter valid . expand

search = concat . map search . expand1

以上の3ケースから、以下の定義がfilter valid . expandと等価なことがわかる：

search :: Matrix [Digit] -> [Matrix [Digit]]
search choiceMatrix
  | not (safe prunedMatrix) = []
  | complete prunedMatrix = [extract prunedMatrix]
  | otherwise      =  concat (map search (expand1 prunedMatrix))
  where prunedMatrix = prune choiceMatrix

なので

solve = filter valid . expand . choices
      = search . choices