SAT solverとSudokuと
SAT solverとは
ある論理式がsatisfiableかどうかを確認してくれるソフトウェアです。
つまり、trueとなる解があるかどうを判定し、ある場合はその1パターンを出力してくれます。
例えば、(x or y) and (x or not y)の場合はxがtrueの場合のみ全体がtrueとなることが分かると思います。よってこの論理式をSAT solverに食わせるとsatisfiableと判定しくれます。
a SAT solver is a computer program which aims to solve the Boolean satisfiability problem. On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable,
Contributors to Wikimedia projects
ソフトウェアの種類は色々とあるのですが、今回はminisatを使用していこうと思います。
Homebrewでもインストールできます。
入力
SAT solverを使用する際には下記のようなtxtを作成する必要があります。SAT solverに与える論理式はCNF (Conjuctive Nomal Form)という形式で書く必要があります。
CNFとは (x1 ∨ x2) ∧ (¬x3 ∨ x4 ∨ ¬x5) ∧ ... の形式で書かれたものを指します。 論理和で作られた論理式を論理積でつなぐ形式になります。
それを表したtxtが下記になります。
p cnf 3 2
1 3 0
-3 2 1 0
1行目の p cnf 3 2
の3は変数の数、 2はclauseの数を表します。
1 3 0
-3 2 1 0
2,3行目はclauseを表します。
数値は変数を表し、マイナスがついているものはその否定を表現します。0はそのclauseの終了を表します。
そして、そのclauseどうしをAndでつなぎます。
よってこのtxtは
(x1 ∨ x3) ∧ (¬x3 ∨ x2 ∨ x1) の論理式を意味しています。
試しに、これを実行してみます。
となり、Satisfiableなことがわかります。
また、第2引数で指定した出力ファイルをみると実際の変数の割当がわかります。
上記は、下記の割当を表しています。
| x1 | true |
| x2 | false |
| x3 | false |
Sudoku
次に数独のルールをCNF形式で表現し、実際の数独の回答が正しいのかどうかを判定するプログラムを作ってみます。
ルール
空いているマスに、1〜9のいずれかの数字を入れる。
縦・横の各列に、同じ数字が重複して入ってはいけない。
太線で囲まれた3×3のグループ（以降「ブロック」と呼ぶ）内に、同じ数字が重複して入ってはいけない。
Contributors to Wikimedia projects
Sudokuのルールの実装
[i][j][k] でCellの情報を表現します。
- i: row
- j: column
- k: number
例: 2行3列が6 = [2][3][6]
空いているマスに、1〜9のいずれかの数字を入れる。
[1][1][1] ∨ [1][1][2] ∨ ... ∨ [1][1][9] ∧ ...
∧... ∨ [9][9][9]
縦・横の各列に、同じ数字が重複して入ってはいけない。
横: (¬[1][1][1] ∨ ¬[1][2][1]) ∧ (¬[1][1][1] ∨ ¬[1][3][1]) ∧ ...
∧ (¬[9][8][9] ∨ ¬[9][9][9])
※x1とx2が両方ともtrueにならないことを表すと¬(x1 ∧ x2) = (¬x1 ∨ ¬x2)なのでこれを使い、CNFで愚直に表現していきます。
太線で囲まれた3×3のグループ（以降「ブロック」と呼ぶ）内に、同じ数字が重複して入ってはいけない。
縦とブロックも横で表した方法を使い表現していきます。
そして、どんな方法でも良いのですが、それぞれのCellと数値の組み合わせに変数を振って行きます。
例: [1][1][1] = x1, [1][1][2] = x2 ...
kooooohe実行
その他
このSAT solverを使うと例えば
- 席替えで上下左右同じ人が現れないようにする
- 時間割りを被りなく作ること
などなどを検証、作成することができます。応用範囲はとても広いので是非触ってみると面白いと思います。