Sudoku solver

数独のソルバをちょっと書き換えた。

問題の持ち方

sudoku = """
000000000
000000000
000000000
000000000
000000000
000000000
000000000
000000000
000000000
"""

データ構造と基本的な解き方

SudokuBoard(list), SudokuSubSquare(SudokuChunk), SudokuChunk(frozenset), SudokuCell(set) を定義した。

  • SudokuBoard は 9x9=81 要素の一次元リスト
  • SudokuChunk は 行、列、 3x3 矩形の キャッシュ
  • SudokuSubSquare は SudokuChunk の 3x3 矩形用の特化クラス
  • SudokuCell はマスを表す

SudokuCell は 自身の数値が確定した際に関係する SudokuChunk 内の SudokuCell から存在しえない数値を順次消していく。 矛盾が発生した際、すなわちマスが空になった際には、例外を投げる。

  • 旧solv1
    def uniq_solver(func):
        def wrapper(self, *args, **kwargs):
            orig = set(self)
            ret = func(self, *args, **kwargs)
            len_new = len(self)
            if orig != self:
                #if(self._board.is_original()):
                #    self._board.print_text()
                dbg_print(f"cell ({self.ri},{self.ci}) updated {orig} to {set(self)}")
            assert len_new
            if len_new == 1:
                for cell in filter(lambda c: self <= c, itertools.chain(self.row, self.col, self.sq)):
                    if id(cell) != id(self):
                        dbg_print(f"target ({cell.ri} {cell.ci}) {cell}")
                        assert cell != self
                        cell -= self
            return ret
        return wrapper

    @uniq_solver
    def __iand__(self,target):
        return super().__iand__(target)

    @uniq_solver
    def __isub__(self,target):
        return super().__isub__(target)

複数数字用ソルバ

属する行/列/3x3矩形内で n個の数字の組み合わせがnマスにしかない場合残マスに同じ数字は入れないはず。 aとbはどちらがどちらか確定できていない場合でも、すくなくとも x にはaもbも入れないパターン

  • 旧solv_n + “3x3矩形用ソルバのパターン2はsolv1でやっとくべき”
class SudokuChunk(frozenset):
    def solv_n(self, n):
        ret = False
        for tpl in itertools.combinations(self.remain, n):
            tpl_set = set(tpl)
            found = set(filter(lambda cell: cell <= tpl_set, self))
            if len(found) == len(tpl):
                for cell in self - found:
                    if not cell.isdisjoint(tpl_set):
                        dbg_print(f"1 ({cell.ri},{cell.ci}) {cell} {tpl_set}")
                        cell -= tpl_set
                        ret = True
            found = set(filter(lambda cell: not cell.isdisjoint(tpl_set), self))
            if len(found) == len(tpl):
                for cell in found:
                    if not cell <= tpl_set:
                        dbg_print(f"2 ({cell.ri},{cell.ci}) {cell} {tpl_set}")
                        cell &= tpl_set
                        ret = True
        return ret

3x3矩形用ソルバ

  • 旧 solv_sqi_line 3x3 矩形用の solv_n の拡張
class SudokuSubSquare(SudokuChunk):
    def solv_n(self, n):
        def _solv_sq(c1, c2):
            for tpl in itertools.combinations(c1.remain, n):
                tpl_set = set(tpl)
                found = set(filter(lambda cell: not cell.isdisjoint(tpl_set), c1))
                if len(found) and found <= c2:
                    for cell in c2 - found:
                        dbg_print(f"3 ({cell.ri},{cell.ci}) {cell} {tpl_set}")
                        cell -= tpl_set
                        ret = True

        ret = super().solv_n(n)
        if n < 4:
            for chunk in itertools.chain(self.rows, self.cols):
                _solv_sq(self, chunk)
                _solv_sq(chunk, self)
        return ret

チェーン矛盾ソルバ

ここまでのソルバで盤面の進展がなくなったときに発動。

  1. 各 Chunk の中に候補 Cell が2つしか残っていない数字を探す。
  2. 2候補のうちどちらかを確定させる
  3. 矛盾が発生するか、運よく解けてしまうまで 通常のソルバを実行する。
  4. 矛盾が発生したルートは偽なので、少なくとももう一方のルートが真であることが確定する。
  • どちらかのルートを選んで、盤面自体をコピーしたのち再帰的にソルバを実行する。矛盾が発生するルートでは例外が発生するのでそれを拾ってコピー前の盤面に対してもう一方の試さなかったルートを確定させる。
  • 運よく解けてしまった場合は、再帰の深さ分元の盤面に正解を反映しつつ戻る。
class SudokuBoard(list):
    def _solv_chain(self, idx, num):
        dbg_print(f"_solv_chain {self[idx]}")
        self[idx] -= set([num])
        self.solv()

    def solv_chain(self):
        for i in ALL_SET:
            for chunk in itertools.chain(self.rows, self.cols, self.sqs):
                found_cells = list(filter(lambda cell: set({i}) <= cell, chunk))
                if len(found_cells) == 2:
                    for cell in found_cells:
                        #print("enter chain")
                        board_new = copy.deepcopy(self)
                        try:
                            board_new._solv_chain(int(cell), i)
                        except:
                            dbg_print("except")
                            cell &= set([i])
                            return
                        else:
                            if board_new.digest() == sum(range(1, SUDOKU_SIZE+1))*SUDOKU_SIZE:
                                dbg_print("dekite shimatta")
                                #for dst in self:
                                #    dst &= board_new[int(dst)]
                                #return
                        finally:
                            pass
                            #print("leave chain")

やること

  • クラス構造のリファクタ
  • ソルバのリファクタ
  • まだないパターンのソルバ実装
    • というか、初期値にChunk内に候補が2つしかない数字の組み合わせがあれば、solv_chain と uniq_solver だけで解ける(と思う)
    • そして、結局人それを総当たりと言う…
    • なので、運よく解けてしまうルートは使いたくなかった。
      • ~~ が、矛盾が発生せずかつ回答にもいたらない時点で solv_chain を再帰せず打ち切ってしまうと、世界一難しい数独は現実的な時間で回答にたどり着かなかった。
        • 片方が偽なら片方が真のパターンを試しているので、運よく正解にたどり着いた際には逆パターンも試してみればよいだけと気付いた。
        • そうすると、複数解を持つ問題も検出できる(はず)
        • 変更後、4倍ほど遅くなったが、世界一難しい数独も正解にたどり着けた。
        • さらに総当たりに近づいたとも言う。
  • kotlin で書き直す。
    • 結局 Python 依存度があがってしまった…
    • せめて、盤面保存の deepcopy は copy on write にしたい…

世界一難しい数独 を実行してみた。

$ time python3 sudokusolver.py
800000000003600000070090200050007000000045700000100030001000068008500010090000400
    12   2 | 23 123 123|1 3     1 3|
    4 6 456|4    5  4  | 56 45  456|
 8        9|7   7      |  9 7 9 7 9|

12  12    3|    12  12 |1       1  |
45  4      |  6  5  4  | 5  45  45 |
  9        |    78   8 | 89 789 7 9|

1          |  3     1 3| 2      1 3|
456     456|4       4  |    45  456|
    7      | 8    9  8 |     8     |
--- --- --- --- --- --- --- --- ---
123      2 | 23  23    |1    2  12 |
4 6  5  4 6|      6    |  6 4   4 6|
  9       9| 89  8  7  | 89  89   9|

123 123  2 | 23        |     2  12 |
  6   6   6|    4    5 |          6|
  9  8    9| 89        |7    89   9|

 2   2   2 |1    2   2 |      3  2 |
4 6 4 6 4 6|      6   6| 56     456|
7 9  8  7 9|     8   89| 89       9|
--- --- --- --- --- --- --- --- ---
 23  23 1  | 23  23  23|  3        |
45  4      |4       4  | 5    6    |
7          |7 9 7     9|  9      8 |

 23  23    |     23  23|  3 1    23|
4 6 4 6    | 5    6 4 6|           |
7        8 |    7     9|  9     7 9|

 23      2 | 23 123 123|     2   23|
 56      56|      6   6|4    5   5 |
7     9 7  |78  78   8 |    7   7  |
--- --- --- --- --- --- --- --- ---
digest: 405
    1    2 |          3|           |
           |     5     |  6 4      |
 8         |7          |          9|

          3|         2 |1          |
    4      |  6        |         5 |
  9        |     8     |    7      |

           |        1  | 2        3|
  6      5 |4          |           |
    7      |      9    |     8     |
--- --- --- --- --- --- --- --- ---
1          | 2    3    |           |
     5  4  |           |          6|
           |        7  | 8    9    |

  3        |           |     2  1  |
      6    |    4    5 |           |
          9| 8         |7          |

 2         |1          |      3    |
           |      6    | 5      4  |
     8  7  |          9|           |
--- --- --- --- --- --- --- --- ---
     2  1  |           |  3        |
 5         |        4  |      6    |
           |  9 7      |         8 |

      3    |     2     |    1      |
4          | 5        6|           |
         8 |           |  9     7  |

           |  3 1      |         2 |
          6|           |4    5     |
7     9    |         8 |           |
--- --- --- --- --- --- --- --- ---
812753649943682175675491283154237896369845721287169534521974368438526917796318452

real    0m4.180s
user    0m4.125s
sys     0m0.016s

解けた。