終章 数独の解き方を見渡す

本編では、同じ数独を十五通りの形へ翻訳しました。盤面を直接たどる方法もあれば、論理式、 多項式、状態遷移、実数の重みへ置き換える方法もあります。どの方法でも、最終的に必要なのは 数独の規則を満たす完成盤面です。ただし、そこへ至る計算と、計算結果から断定できる範囲は 同じではありません。

十五の翻訳を比べる

次の表は、各章でマスと規則を何に置き換え、掲載実装がどのように答えを探したかをまとめたものです。 Partの区分は中心となる見方を示します。たとえばExact Coverは専用の表現を使いますが、その表を 解く過程には分岐とバックトラックがあります。一つの手法が一つの分類だけに収まるわけではありません。

数独の翻訳と計算方法

方法	マスと規則の表現	掲載実装の計算	掲載例
バックトラック	盤面と各マスの候補	候補を仮置きし、行き詰まった枝から戻る	9×9、Python
Exact Cover	数字を置く候補と、その候補が覆う四種類の条件	Algorithm Xで条件を覆う行を分岐させる	9×9、Python
Prolog	論理変数、候補を求める述語、重複を禁じる規則	単一化と失敗時のバックトラックで候補を試す	9×9、SWI-Prolog
miniKanren	論理変数と、各単位を順列にする関係	遅延ストリームから条件を満たす値の組を列挙する	4×4、Python kanren
制約プログラミング	有限領域変数と all_different 制約	制約伝播で候補を減らし、残りを探索する	9×9、MiniZincとGecode
ASP	value/3 の候補、choice rule、整合性制約	条件を満たす安定モデルを列挙する	9×9、clingo
SAT	数字を置く候補を表す真偽変数とCNF節	CDCLソルバーで充足する割り当てを探す	9×9、PySATとMiniSat
SMT	各マスの整数変数、値域、Distinct、初期配置の式	整数の理論を含む論理式の充足可能性を調べる	9×9、Z3
BDD	真偽変数で表した規則と解集合の縮約グラフ	グラフを構築し、グラフをたどってモデル数を求める	4×4、Python dd
モデル検査	盤面を状態、一マスを埋める操作を状態遷移として表す	完成状態へ到達する経路を有界モデル検査で探す	9×9、nuXmv
整数計画法	数字を置く候補を表す0-1変数と線形等式	MIPソルバーで実行可能解を探す	9×9、HiGHS
Boolean Gröbner基底	0-1候補と数独の規則を表す多項式方程式	Gröbner基底を計算し、連立方程式の根を復元する	4×4、SymPy
QUBO	0-1候補と、規則違反を加点する二次式	焼きなましで低エネルギー状態をサンプリングする	4×4、neal
反復射影	候補の実数配列、局所制約集合、複製間の合意集合	Difference Mapで二つの集合への射影を繰り返す	4×4、NumPy
因子グラフ	マスを表す変数、行・列・ブロックの因子、候補の重み	ループ付きグラフ上でメッセージを反復更新する	4×4、Python

結果から何を断定できるか

完成盤面を一つ得ることと、解がないことや一意解であることを示すことは別です。掲載実装について、 判定できる範囲を次の表に示します。「完了時」は、全探索、基底計算、または定めた上界までの検査が 最後まで終わった場合を指します。「二解で判定」は、異なる二盤面を得れば複数解と確定できますが、 一盤面しか得られなくても一意解とは限らないという意味です。

掲載実装が判定できる範囲

方法	解がない場合	一意性	列挙・数え上げ
バックトラック、Exact Cover、Prolog、miniKanren、制約プログラミング	全探索の完了時に unsat	二解まで探し、探索終了も確認して判定	掲載実装は最大二解を取得する
ASP	全モデル探索の完了時に unsat	モデル数と探索完了を確認して判定	掲載実装は最大二モデルを取得する
SAT	ソルバーが UNSAT を返せば判定	最初のモデルを除外して再判定	掲載実装は最大二解を取得する
SMT	ソルバーが unsat を返せば判定	最初のモデルを除外して再判定	掲載実装は最大二解を取得する
BDD	モデル数が0なら判定	モデル数が1なら判定	グラフから全解数を直接求められる
モデル検査	完全な上界まで到達経路がなければ判定	最初の完成状態を除外して再検査	掲載実装は最大二解を取得する
整数計画法	ソルバーが Infeasible を返せば判定	最初の実行可能解を除外して再判定	掲載実装は最大二解を取得する
Boolean Gröbner基底	基底計算と根の復元の完了時に判定	復元した根の個数で判定	掲載実装は全解を復元する
QUBO	焼きなましでは判定できない	二解で複数解とは判定できる。一解では未判定	標本中の相異なる解を得る。全解数とは限らない
反復射影	判定できない	判定できない	一回の試行で一盤面を探す
因子グラフ	判定できない	判定できない	掲載実装には列挙機構がない

この違いは、モデル名だけでは決まりません。QUBOでも厳密な最適化器が最小値を証明すれば判定の 範囲は変わります。反対に、完全な探索方法でも、時間制限や解数の上限で打ち切れば、そこから先の 解や解なしを断定できません。モデル、ソルバー、終了条件を一組として確認する必要があります。

目的から方法を選ぶ

数独の解を一つ得ることが目的なら、まずは盤面を直接扱うバックトラックで十分です。探索の仕組みを 自分で確かめられ、共通検証器まで含めても実装を短く保てます。規則の追加や変更が多い場合は、 制約プログラミング、SMT、ASPのように、規則をモデルへ書いて探索をソルバーへ任せる方法が扱いやすく なります。線形の目的関数も加えたい問題なら、整数計画法が候補になります。

解なしや一意性を示したい場合は、完全な探索またはソルバーの完了状態を確認できる方法を選びます。 一意性には、一つ目の解を得るだけでなく、二つ目を探して存在しないことを確かめる処理が必要です。 全解数そのものが必要なら、解集合をグラフとして保持して数えられるBDDが、この連載では最も直接的な 例です。ただし、BDDの大きさは変数順と問題構造に左右されます。

QUBO、反復射影、因子グラフは、規則をエネルギー、集合の交点、局所的な重みの交換として捉え直します。 掲載実装では、検証を通る盤面が得られれば解の存在を示せますが、得られなかっただけでは解なしとは 言えません。これらは厳密解法の代わりとしてではなく、別の計算表現から候補へ到達する過程を観察する 例として読むと、役割が明確になります。

翻訳と検証を分ける

どの方法でも、計算手続きが保証するのは、渡されたモデルや規則に対する結果です。CNFのモデル、 安定モデル、多項式の根、ゼロエネルギー状態が数独の完成盤面と対応するには、変換が正しくなければ なりません。 本編では、初期配置と行、列、ブロックの規則をモデルへ入れ、得た盤面を共通検証器でも調べました。

この二段階を分けると、問題の所在を追いやすくなります。計算が完了しない場合は探索と終了条件を、 答えを返しても盤面が規則を破る場合は変換または復元を調べます。数独を別の問題へ翻訳して解くとき、 最後まで共通するのはこの確認です。