Thinking Functionally with Haskell勉強メモ: 第5章3 不確定なマスを再帰的に「みなし確定」させて枝刈り
前回のsolve
は「すでに確定したマスの値を使って枝刈り」の後に「残った各マスの取り得る値の全探索」という解決方法だった。
これでも相当な効率化が図られているが、「残った各マスの取り得る値の全探索」のほうにまだまだ改善の余地が残されている。例えば4つのマスがひとつの行に未確定で残されている場合、全探索だと調べる組み合わせの総数はだが、実際にはで探索できる。
一つの未確定のマスを「確定した」とみなしてできる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
はあるリストが要素数1かどうかを調べる関数。Don't Careパターンマッチがなかなかかっこいい。
complete
はあるMatrix [Digit]
の[Digit]
部分がすべて要素数1か、つまりその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