SATソルバーを用いて，パズル・数独を解いたのでここにまとめます．

MacとLinux両方で本記事の数独ソルバーが動くことを確認しています．

記事の内容が，SATソルバーを触ったことのない人にとって難しくならないように努めます．

SATとは

SAT(boolean SATisfiability testing)は，命題論理式の充足可能性判定¹のことで，CNF (Conjuctive Normal Form) を扱うことが一般的とされています．

CNF式とは

CNFは論理学とかで出てくる連言標準形のことです．

用語の説明をします．

リテラル : 変数x，またはその否定$\lnot$xのこと
節 : リテラルを論理和$\lor$で結合した論理式のこと
CNF式 : 節を論理積$\land$で結合した論理式のこと

CNFの例を以下に示します．もちろん，変数$x$は 0 か 1 をとります．

$$(x_1 \lor \lnot x_2) \land x_3 \land (\lnot x_1 \lor \lnot x_2) $$

以上を満たす解 (全体が1となるような値割り当て) は，$x_1 = 1,x_2 = 0,x_3=1$があります．

SATソルバーとはこれを解くソルバーのことです．

ソルバーのインストール

Mac，Linuxなら以下のシェルスクリプトを実行するとSATソルバー clasp3.3.4 が手に入ります．

install_clasp334.sh

cd /usr/local/src
wget https://github.com/potassco/clasp/releases/download/v3.3.4/clasp-3.3.4-source.tar.gz
tar xvzf clasp-3.3.4-source.tar.gz
cd clasp-3.3.4
cmake -H. -B/usr/local/src/clasp-3.3.4
cmake --build /usr/local/src/clasp-3.3.4
cmake --build /usr/local/src/clasp-3.3.4 --target install
cp -p bin/clasp /usr/local/bin/clasp334
ln -s clasp334 clasp

DIMAC CNF形式

ソルバーのCNF式の入力は，DIMACS CNF形式と呼ばれる整数列で簡潔に記述されることが多いです．

$x_1$を1，$x_2$を2，$x_3$を3という整数に割り当てたとき，上記のCNF式は以下のようなDIMACS CNF形式でかかれます．

sample.cnf

p cnf 3 3
1 -2 0
3 0
-1 -2 0

$x_1$の否定は-1と表現します．

DIMACS CNFは「p cnf "変数の数" "節の数"」から始まります．

各行が節を表していて，節の終わりには0を書いてあげます．

簡単ですね．

端末やターミナルから，以下のコマンドで clasp を起動して解くことができると思います．
$ clasp sample.cnf

数独を解く準備

上記のシェルスクリプトのように，ソルバーはインストールしておいてください．

では，数独を解く準備をしていきます．

具体的には，問題の情報を詰め込んだCNFを作ります．²

問題の条件

Wikipedia³ によると，以下のルールに基づいたパズルだということです．

空いているマスに1〜9のいずれかの数字を入れる
縦・横の各列及び、太線で囲まれた3×3のブロック内に同じ数字が複数入ってはいけない

自分は，こういう風にリテラルを作りました．

左上に入るマスにある数字$x(1 \leq x \leq 9)$が入るとき，そのリテラルを$x$とする．

その右のマスにある数字$y(1 \leq y \leq 9)$が入るとき，$y+9$となるような数字をリテラルにする...って急に言われても困りますよね．．．

例えば，写真の数独をDIMACS CNFで表現する時，

5 0 # 左上の5
12 0 # その右の3
43 0 # 一番上の行の7
87 0 # 左上から一つ下の6
...

みたいな感じでリテラルを与えました．

ルールの条件

数独は"同じ行に同じ数字が入ってはいけない．"というルールでした．

それでは"一番上の行に，1は1回しか現れない"という制約を書いてみましょう．

# 一番上の行で，1は一回以上現れる．(at-least-one制約)
1 10 19 28 37 46 55 64 73 0

# 一番上の行で，1はたかだか一回現れる．(at-most-one制約)
-1 -10 0
-1 -19 0
-1 -28 0
-1 -37 0
-1 -46 0
-1 -55 0
-1 -64 0
-1 -73 0
-10 -19 0
-10 -28 0
-10 -37 0
-10 -46 0
-10 -55 0
-10 -64 0
-10 -73 0
-19 -28 0
-19 -37 0
...
(全ての組み合わせを重複なく書いてください！) 
...
-46 -55 0
-46 -64 0
-46 -73 0
-55 -64 0
-55 -73 0
-64 -73 0

at-least-one制約はなくても解けるのですが，あった方が早く解けるので入れてみてください．

ここは「1 または　10 または　19　または ... または 73」ってイメージです．

at-most-one制約は，上記のようにpairwise法で書き下したとき，多分，${}_9C_2$節あります．

ここは「(1の否定または　10の否定)　かつ　(1の否定　または　19の否定)　...」って感じです．

これを1だけでなく，9までの数字全てで作ります．

さらに，行だけでなく列，ブロックに関しても作っていきます．

すると，以下のようなcnfファイルが完成します．

変数の数は729，節数は12018のCNFになりました．

数独を解く

練習がてらpythonで書いてみました．
プログラムは以下のようにして数独の解を求めています．

Encording : txtファイルの数独情報からcnfファイルを作る
Solving : システムコールでSATソルバー clasp を起動してcnfファイルを解く
Decording : clasp のログを解析して，数独の答えを表示する

GitHubに置きました．

数独の問題は，以下のようにファイルを作ってあげてください．

toi_001.txt

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

実行結果を以下に載せます．

プログラムを実行したら，解きたい問題ファイルの入力を求められますので，ファイル名を入力してください．

出力

$ python numpre_solver.py 
解きたい数独問題のパス : toi_001.txt
********************SAT-based Sudoku Solver********************
1. Encording
  square number plate problem : 3^2
  [pazzle problems]
    _____________________
    | - - - - - - - 7 - |
    | 1 - 5 - 3 6 4 - 9 |
    | - 7 4 9 - - 5 - - |
    | - - - - - 5 8 - - |
    | - 1 - 3 - - - - 5 |
    | 7 - - - - 8 1 - - |
    | 6 4 - - - - - - 7 |
    | - 3 - 6 2 - - 8 4 |
    | - - - 5 9 - - - 3 |
    _____________________

 2. Solving...
   solver :clasp
   solved!

 3. Decording
  Solving Time       : 0.001s

   [pazzle answer]
   _____________________
   | 9 6 2 4 5 1 3 7 8 |
   | 1 8 5 7 3 6 4 2 9 |
   | 3 7 4 9 8 2 5 6 1 |
   | 4 9 6 1 7 5 8 3 2 |
   | 2 1 8 3 6 9 7 4 5 |
   | 7 5 3 2 4 8 1 9 6 |
   | 6 4 9 8 1 3 2 5 7 |
   | 5 3 1 6 2 7 9 8 4 |
   | 8 2 7 5 9 4 6 1 3 |
   _____________________
***************************************************************

ここで出てきている Solving Time とは，SATソルバーがCNFを解いた時間です．

この問題では0.001秒なので，人間が解くより早いかもしれません．

世界一難しい数独は，0.006秒で解けました．

それ以外の問題で，問題集にある問題を800問ほど解きましたが，Solvingの平均は0.002秒切ってる感じでした．

中古のThinkPad X240ですらそれくらいで解けるので，皆さんの手元のマシンの方がもう少し早いと思います．

ちなみに，制約プログラミング以外 (C/C++/Java/Python) だけで作られたソルバーでこれより早く解けてそうな記事は，自分の見た感じなかったので，あれば教えてください．

アルゴリズム書いていくよりも，SATソルバー使ったらとても早かったよ，って言うお話です．

16*16の数独

プログラムは一辺16マスの数独にも対応しています．

toi_002.txt

5,-,-,-,-,-,9,14,10,2,-,-,-,-,-,3
10,-,16,-,13,4,6,-,-,11,3,9,-,14,-,1
-,11,14,13,16,-,-,1,12,-,-,8,4,6,9,-
3,-,9,-,8,-,-,-,-,-,-,4,-,10,-,15
8,12,-,-,14,-,-,10,13,-,-,1,-,-,6,16
-,-,-,11,-,1,7,-,-,9,8,-,14,-,-,-
-,13,1,7,-,9,-,-,-,-,14,-,5,2,3,-
4,-,-,5,-,-,-,-,-,-,-,-,1,-,-,11
6,-,-,10,-,-,-,-,-,-,-,-,11,-,-,5
-,5,13,15,-,16,-,-,-,-,4,-,3,1,14,-
-,-,-,2,-,15,1,-,-,12,13,-,6,-,-,-
1,4,-,-,5,-,-,11,9,-,-,3,-,-,15,13
2,-,10,-,7,-,-,-,-,-,-,13,-,11,-,8
-,8,5,14,1,-,-,12,4,-,-,10,2,16,7,-
9,-,15,-,3,10,14,-,-,6,11,16,-,5,-,4
12,-,-,-,-,-,13,16,1,5,-,-,-,-,-,14

出力

$ python numpre_solver.py 
解きたい数独問題のパス : toi_002.txt
********************SAT-based Sudoku Solver********************
1. Encording
  square number plate problem : 4^2
  [pazzle problems]
    _____________________
    | 5 - - - - - 9 14 10 2 - - - - - 3 |
    | 10 - 16 - 13 4 6 - - 11 3 9 - 14 - 1 |
    | - 11 14 13 16 - - 1 12 - - 8 4 6 9 - |
    | 3 - 9 - 8 - - - - - - 4 - 10 - 15 |
    | 8 12 - - 14 - - 10 13 - - 1 - - 6 16 |
    | - - - 11 - 1 7 - - 9 8 - 14 - - - |
    | - 13 1 7 - 9 - - - - 14 - 5 2 3 - |
    | 4 - - 5 - - - - - - - - 1 - - 11 |
    | 6 - - 10 - - - - - - - - 11 - - 5 |
    | - 5 13 15 - 16 - - - - 4 - 3 1 14 - |
    | - - - 2 - 15 1 - - 12 13 - 6 - - - |
    | 1 4 - - 5 - - 11 9 - - 3 - - 15 13 |
    | 2 - 10 - 7 - - - - - - 13 - 11 - 8 |
    | - 8 5 14 1 - - 12 4 - - 10 2 16 7 - |
    | 9 - 15 - 3 10 14 - - 6 11 16 - 5 - 4 |
    | 12 - - - - - 13 16 1 5 - - - - - 14 |
    _____________________

 2. Solving...
   solver :clasp
   solved!

 3. Decording
  Solving Time       : 0.064s

   [pazzle answer]
   _____________________
   | 5 15 4 8 11 12 9 14 10 2 1 6 16 7 13 3 |
   | 10 2 16 12 13 4 6 15 7 11 3 9 8 14 5 1 |
   | 7 11 14 13 16 3 10 1 12 15 5 8 4 6 9 2 |
   | 3 1 9 6 8 2 5 7 14 13 16 4 12 10 11 15 |
   | 8 12 3 9 14 5 11 10 13 4 2 1 7 15 6 16 |
   | 16 10 6 11 2 1 7 3 5 9 8 15 14 13 4 12 |
   | 15 13 1 7 12 9 8 4 6 16 14 11 5 2 3 10 |
   | 4 14 2 5 15 13 16 6 3 7 10 12 1 9 8 11 |
   | 6 9 12 10 4 7 3 13 16 1 15 14 11 8 2 5 |
   | 11 5 13 15 6 16 12 8 2 10 4 7 3 1 14 9 |
   | 14 3 8 2 10 15 1 9 11 12 13 5 6 4 16 7 |
   | 1 4 7 16 5 14 2 11 9 8 6 3 10 12 15 13 |
   | 2 16 10 3 7 6 4 5 15 14 12 13 9 11 1 8 |
   | 13 8 5 14 1 11 15 12 4 3 9 10 2 16 7 6 |
   | 9 7 15 1 3 10 14 2 8 6 11 16 13 5 12 4 |
   | 12 6 11 4 9 8 13 16 1 5 7 2 15 3 10 14 |
   _____________________
***************************************************************

難しめの問題を選んでしまったのか，0.064秒もかかっていました．

もしかしたら，16*16の問題はこんなものかもしれません．

他のソルバーだと，どれくらいで解けるんでしょうね．

多分25*25の数独も解けます．(疲れたので解く気なし．)

まとめと今後の予定

SATソルバーを知らない，使ったことがない人に向けて書いてみました．

アレも入れたい，コレも入れたいっていう欲求を抑えながら書いたので，本当の最低限しか書いてないと思います．

上手くいかない，ここ意味がわからないよ！ってことがあれば，教えてください．

ソルバーをこれ以上高速化する予定はありませんが，いくつか早くできそうな方法は知っているので，暇ができたら試してみます．

今は，このソルバーを使って，数独を解いてくれるアプリとか，サイトを立ち上げることに興味を持っています．

【追記　2020/01/12】
AWS + php + SATソルバーを用いて
9x9の数独を解いてくれるサイトを立ち上げました！
http://okmt1230z.com/sudoku/sudoku.html

この記事に出てくる用語の説明などに関しましては，人工知能学会特集記事であるこちらや Wikipedia に基づいています． ↩
この記事は情報処理学会のSATとパズルを参考にしています． ↩
なんでも載ってるけど，研究室内で引用したら怒られるやつです． ↩

数独を一瞬で解く by SATソルバー