Qiita Teams that are logged in
You are not logged in to any team

Log in to Qiita Team
Community
OrganizationAdvent CalendarQiitadon (β)
Service
Qiita JobsQiita ZineQiita Blog
17
Help us understand the problem. What is going on with this article?
@okmt1230z

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

More than 1 year has passed since last update.

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

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

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

SATとは

SAT(boolean SATisfiability testing)は,命題論理式の充足可能性判定1のことで,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を作ります.2

問題の条件

Wikipedia3 によると,以下のルールに基づいたパズルだということです.

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

sudoku.png

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

左上に入るマスにある数字$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で書いてみました.
プログラムは以下のようにして数独の解を求めています.

  1. Encording : txtファイルの数独情報からcnfファイルを作る
  2. Solving : システムコールでSATソルバー clasp を起動してcnfファイルを解く
  3. 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


  1. この記事に出てくる用語の説明などに関しましては,人工知能学会特集記事である こちら や Wikipedia に基づいています. 

  2. この記事は情報処理学会のSATとパズル を参考にしています. 

  3. なんでも載ってるけど,研究室内で引用したら怒られるやつです. 

17
Help us understand the problem. What is going on with this article?
Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
okmt1230z
SATソルバー VFS Flutter/Dart/JavaScript/Java/C/C++/python CTF(web)

Comments

No comments
Sign up for free and join this conversation.
Sign Up
If you already have a Qiita account Login
17
Help us understand the problem. What is going on with this article?