この記事は圧倒的令和ッ！！ぴょこりんクラスタ Advent Calendar 2019のために書いたものです。
このAdvent Calendarが何なのかについては、主催者による紹介記事を見てください。
サマリ
NuSMVに数独を解かせようとしたが、ちょっと難しくなるとOOM Killerに殺されて解けなかったのでSATソルバに解かせた。道具は目的に合ったものを使おう。
はじめに
世の中にはモデル検査という技術がある。平たく言えば、プログラムをモデル化したもの*1に対し、どのような性質(例えば、デッドロックしないかどうかとか)を持つかを網羅的に調べる技術で、
航空機や自動車、鉄道など、特に安全性が求められるソフトウェアで使われることが多い。
事例はここに多少まとまっており、
国内ではスバルやJAXA、国外では、ボンバルディア、Airbus、Microsoftが使っている。
モデル検査ツールは、切り出す側面に応じて様々な種類がある。
以下に例を示す。
- SPIN: 複数のプロセスの通信を、オートマトンでモデル化したものを検証するツール。
- NuSMV: プログラムの状態遷移をモデル化したものを検証するツール。
- UPAAL: プログラムの時間遷移をモデル化したものを検証するツール。
いろいろ種類はあるが、モデル検査ツールが共通して持つ特徴は以下の通り。
- 検証対象の性質は何らかの論理式で記述される
- 性質を持つかどうかは、論理式を満たすかどうかで表される
- 論理式を満たすかどうかを、網羅的に検査する
- 論理式を満たさない場合は、反例を1つ出力する
面白いのが4番目の反例を出力する性質で、これをうまく使えばちょっとしたクイズを解くことができる。
要は、満たしてほしい性質(=クイズの回答)の否定を論理式として与えて、
反例として回答を出させる、ということである。
というわけで、おなじみの数独をモデル検査ツールに解かせてみることにする。
使うのは文法がシンプルで、モデルも(たぶん)わかりやすいNuSMVとする。
NuSMVについて
入手
NuSMVは、SMVのなかで、唯一商用化・無料で使えるものである。
ダウンロードの際にフォームが出るが、CAPTCHAだけ入力すればダウンロードできる。
ビルドは大変なので、バイナリを使うのが楽。
Minisat版でもZchaff版でもどっちでもいいと思うが、自分はMinisatのほうを使った。
モデル化
素直に、数独の各マスの値が変化する、というモデル化を行う。
NuSMVでモデル化するにあたり、とりあえずやるだけであれば、きちんと文法や機能を使いこなす必要はないので、
今回使っているものだけ、例を用いて説明する。
例として、数独の1行、2つ空欄の場合のソースコードを示す。
-- a0 a1 a2 a3 a4 a5 a6 a7 a8
-- 7 8 3 1 4 2 9 x x のa7とa8を埋める
-- (a7, a8) = (5, 6)もしくは(6, 5)が答え。
MODULE main -- Cで言うところのmain関数的表現。とりあえず一番上に書いておけば良い。
DEFINE -- Cでいうところの`
a0 := 7; -- 文末にセミコロンを置く
a1 := 8;
a2 := 3;
a3 := 1;
a4 := 4;
a5 := 2;
a6 := 9;
VAR -- 変数宣言。取りうる範囲まで指定する必要がある。SMVは網羅検査するので、なるべく取りうる範囲を絞る。
a7 : {0, 5, 6}; -- 整数値が連続している場合は、x: a..b(pythonと違ってa <= x <= b)と書いてもよいが、
a8 : {0, 5, 6}; -- 今回は歯抜けになっているので、{}でくくって書く
ASSIGN -- 状態遷移ルール(=変数の初期値と変化ルール)を記述する。
init(a7) := 0; -- 初期値
next(a7) := case -- 次に何の値を取るか
-- a0 + a1 + a2 + a3 + a4 + a5 + a6 + a8 = 44 : 1; -- <条件> : <次の値>というフォーマットで書く。
-- 数独では、値が変化するのに必要なルールは特にないので、上の条件文はコメントアウトしておく。
TRUE : {5, 6}; -- 最後に必ずTRUEの分岐を書く必要がある。TRUEだけだと、ランダムにどちらか選ばれる。
esac;
init(a8) := 0; -- 初期値
next(a8) := case -- 次に何の値を取るか
TRUE : {5, 6}; -- ランダムにどちらか選ばれる。
esac;
SPEC
!EF( -- EFは、将来一度でも成立する、という意味。!付きなので、将来一度も成立しない、と読む。
!(a7 = a8) -- a7とa8が等しくならない。つまり、a7とa8が等しくならないことはない、という性質を検証する。
)
これを実行するとこういう出力が出る。
a7 = 5, a8 = 6なので、期待通り解けている。
$ ./NuSMV-2.6.0-Linux/bin/NuSMV test.smv
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:36:56 2015)
*** Enabled addons are: compass
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@list.fbk.eu>.
*** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>
*** Copyright (c) 2010-2014, Fondazione Bruno Kessler
*** This version of NuSMV is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado
*** This version of NuSMV is linked to the MiniSat SAT solver.
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson
-- specification !(EF !(a7 = a8)) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
a7 = 0
a8 = 0
a6 = 9
a5 = 2
a4 = 4
a3 = 1
a2 = 3
a1 = 8
a0 = 7
-> State: 1.2 <-
a7 = 5
a8 = 6
NuSMVで数独を解いてみる
その1: 簡単なやつ
先程の例をそのまま拡張してやればよいが、いかんせんマス目が多くて大変なので、
SMVスクリプトを生成させて、それを実行することにする。
ジェネレータのソースコードは以下の通り。
数独を解くNuSMVソースコードのジェネレータ · GitHub
では、まずは肩慣らしに簡単なやつを解いてみよう。
https://kachikachi.net/numberplace/ で、予め50個/81個の
数字が埋まっている問題を生成して、NuSMVに解かせてみる。
ソースコードはこれ。
簡単な数独を解くNuSMVソースコード · GitHub
問題はこれで、
A 0 8 6 1 0 0 0 2 0
B 3 2 4 0 0 0 1 0 5
C 7 5 1 3 2 0 9 8 6
D 2 4 3 9 8 6 0 0 1
E 0 0 0 7 0 1 0 0 0
F 5 0 0 2 4 3 8 6 9
G 6 9 8 0 1 7 4 3 2
H 1 0 5 0 0 0 6 9 8
I 0 3 0 0 0 9 5 1 0
NuSMVが出した回答は以下で、
-> State: 1.2 <-
A0 = 9
A4 = 7
A5 = 5
A6 = 3
A8 = 4
B3 = 6
B4 = 9
B5 = 8
B7 = 7
C5 = 4
D6 = 7
D7 = 5
E0 = 8
E1 = 6
E2 = 9
E4 = 5
E6 = 2
E7 = 4
E8 = 3
F1 = 1
F2 = 7
G3 = 5
H1 = 7
H3 = 4
H4 = 3
H5 = 2
I0 = 4
I2 = 2
I3 = 8
I4 = 6
I8 = 7
これをあてはめるとこうなる。合ってるっぽい。
A 9 8 6 1 7 5 3 2 4
B 3 2 4 6 9 8 1 7 5
C 7 5 1 3 2 4 9 8 6
D 2 4 3 9 8 6 7 5 1
E 8 6 9 7 5 1 2 4 3
F 5 1 7 2 4 3 8 6 9
G 6 9 8 5 1 7 4 3 2
H 1 7 5 4 3 2 6 9 8
I 4 3 2 8 6 9 5 1 7
状態数は
cat sudoku_sp_easy.smv | grep TRUE | perl -lane 's/\{//g; s/\};//g; s/,//g; s/TRUE ://g; s/ //g; print' | perl -lane 'BEGIN{$count=1;} $count *= (length $F[0]); END{print $count}'
166kほど。
その2: ちょっと難しいやつ
次に、https://kachikachi.net/numberplace/ で、予め35個/81個の
数字が埋まっている問題を生成して、NuSMVに解かせてみる。
この問題自体は、そのマスに入り得る数が1個しかないものから順に埋めていくだけで
解けるようなので、そんなに難しくはなさそう。
A 3 0 2 0 0 5 7 4 9
B 0 0 6 0 0 9 0 1 2
C 0 0 4 3 0 2 0 0 0
D 0 0 0 9 0 0 0 3 0
E 4 0 7 0 3 0 6 0 8
F 0 3 0 0 0 6 0 0 0
G 0 0 0 1 0 3 8 0 0
H 8 6 0 4 0 0 1 0 0
I 1 2 3 6 0 0 4 0 7
生成したソースコードはこれ。
ちょっと難しい数独を解くNuSMVソースコード · GitHub
メモリ8GB積んだVMで動かしているが、OOM killerに殺されたようでダメだった・・・
状態数は
cat sudoku_sp_mid.smv | grep TRUE | perl -lane 's/\{//g; s/\};//g; s/,//g; s/TRUE ://g; s/ //g; print' | perl -lane 'BEGIN{$count=1;} $count *= (length $F[0]); END{print $count}'
2.49593749508299e+19
2.5 * 10^19くらいあるようで、網羅検査すればメモリ使い果たすよなという感がある。
金槌を持つと何でも釘に見えてしまうような使い方はよろしくないね。
SATソルバに解かせてみる
目的外利用の限界を感じたが、ちょっと悔しいのでSATソルバに解かせてみることにする。
SATソルバはSMVと違って網羅検査が目的ではなく、条件を満たす例を1つ出してくれるものだ。
条件を満たす例を1つ出すという目的内利用なので、SMVよりは当然速いはずだ。
使ったソルバはMicrosoft Researchが出しているZ3である。
解き方はSMVのときとほとんど変わらなくて、初期状態と満たすべき条件を書き下すだけである。
ソースコードは以下の通り。
z3を使って数独を解くソースコード · GitHub
で、早速ちょっと難しいやつを解かせてみる。今度は解けた。
A 3 1 2 8 6 5 7 4 9
B 5 8 6 7 4 9 3 1 2
C 9 7 4 3 1 2 5 8 6
D 6 5 8 9 7 4 2 3 1
E 4 9 7 2 3 1 6 5 8
F 2 3 1 5 8 6 9 7 4
G 7 4 9 1 2 3 8 6 5
H 8 6 5 4 9 7 1 2 3
I 1 2 3 6 5 8 4 9 7
今度は30個/81個埋まってる問題を解かせてみるが、これも難なく解けた。
ちなみに、問題がこれで、
A 0 5 0 0 0 1 0 7 0
B 1 0 0 0 0 2 0 0 0
C 2 0 7 0 0 4 1 0 0
D 0 2 0 0 0 0 9 1 6
E 0 0 5 0 0 0 2 0 0
F 9 1 6 0 0 0 0 3 0
G 0 0 1 7 0 0 5 0 3
H 0 0 0 5 0 0 0 0 1
I 0 4 0 9 0 0 0 2 0
回答がこれである。
A 3 5 4 6 9 1 8 7 2
B 1 6 9 8 7 2 3 5 4
C 2 8 7 3 5 4 1 6 9
D 7 2 8 4 3 5 9 1 6
E 4 3 5 1 6 9 2 8 7
F 9 1 6 2 8 7 4 3 5
G 6 9 1 7 2 8 5 4 3
H 8 7 2 5 4 3 6 9 1
I 5 4 3 9 1 6 7 2 8
もっと難しい問題も解けるようなので、当然と言えば当然か。でもいざ目の当たりにすると感動するね。
おわりに
SMVは状態遷移が手軽に書けてよいが、目的に合わせて使おう。
SMVは網羅的に調べてくれるのがよいところであって、こういうクイズを解く道具ではない。
