簡単なSMT&SATソルバーを書いて4x4数独を解く
作成日: 2024-10-22
SMTソルバーとSATソルバーを実装したので、その実装のメモです。リポジトリはこちら。
主に次の記事を参考にしました。
SMTソルバー
SMTソルバーは論理式を満たす変数を求めるソルバーです。
X, Yが0か1の変数として、命題X≠YをSMTソルバーの表現で表すと次のようになります。この命題を満たすのは(X, Y)=(0, 1),(1, 0)です。どちらかを発見して、SMTソルバーは終了します。
(int x 0 1)
(int y 0 1)
(not (eq x y))数値表現
数値表現を真か偽に割り当てるように論理式を変形します。x0が偽ならX=0、真ならX=1です。X=Yの部分が次のように翻訳されます。数値表現には様々ありますが、今回は一番単純な表現を実装しています。
(not (or (and x0 y0) (and (not x0) (not y0))))CNF表現
さらに、命題をCNF(和積標準形)に変形します。ORの部分は変数を補うことによって、命題の数を抑えてCNFに変形することが出来ます。
!x0 or !$or_1
!y0 or !$or_2
$or_1 or $or_2
x0 or !$or_3
y0 or !$or_4
$or_3 or $or_4SAT表現
最後に変数を数字に置換することで、SATソルバーが解ける形になります。SMTソルバーは命題をSAT表現に変換して、割り当てられた結果を元の変数に戻します。
c vars ["x0", "$or_1", "y0", "$or_2", "$or_3", "$or_4"]
-1 -2 0
-3 -4 0
2 4 0
1 -5 0
3 -6 0
5 6 0SATソルバー
最後に、SAT表現を解けばタスク完了です。
単純なDPLLアルゴリズムと、より賢いCDCLアルゴリズムを実装しました。
DPLLは単純なバックトラックです。50命題変数ぐらいなら解けますが、実用性はありません。
CDCLはDPLLに矛盾学習とバックジャンプを実装したものです。CDCLは4x4の数独の約1000変数が解けました。
9x9の数独は、およそ50000変数のSATになっており、単純なCDCLでは解けませんでした。SAT表現への変換の工夫と、CDCLの変数決定ヒューリスティックが必要になります。
世の中にあるMiniSatやZ3はかなり大きめの問題を解けるので素晴らしいですね。
関連
SMTソルバーを使って自作ペンシルパズルを解く話です。