ペンパ勢が SAT ソルバーを触ってみました。その備忘録と感想です。
筆者のスペック
・ペンシルパズルはそれなりに解け、それなりに造詣が深い (つもり)
・プログラミングは、競プロをそれなりにたしなんでいる (青コーダー)
・でも、情報にまつわる知識はさっぱり (←重要)
注意という名の言い訳
あくまで自分のためのまとめと、感想を書いただけの記事です。技術的なことは何も書いてません。
最近、ネットで何か調べものをしたとき、知りたいことが書いてないただの感想の記事を見つけて「そうじゃないんよ、そうじゃないんよ...」ってなることが多く、困ってます。残念ながら、この記事はその「そうじゃない」方ですが、それでもいい人は読んでください。
SATソルバーってなんじゃい
"SAT" とは SATisfiability の略らしい。日本語にすると「充足可能性問題」。もうちょっと噛み砕くと、真か偽かの論理変数とそれについての命題論理式を与えて、変数の真偽をうまく決めることで全体を真にできるか、という問題。イメージとしては、連立方程式の解が存在するかを判定する感じ (って認識してるけど、あってるかは知らん)。
で、それを解いてくれるのが SAT ソルバーくん。使い方としては、まず人間が論理式を用意します。次に、それを SAT ソルバーくんに投げつけます。すると、SAT ソルバーくんは解があるかどうかを判定し、解があれば具体的にひとつ示してくれます。すごい！
ちなみに、ぼくは動作原理を全然理解しておらず、ただの便利な人と思ってます。一応なんとなくやってそうなこととして
・すぐわかる変数はすぐ決める
・これ以上わかんなくなったら適当に仮置きする (バックトラック？)
というのはあるっぽい？わからん...まあ意識しておくとといいことあるかもしれない。
ペンシルパズルを解く
ペンシルパズルは、だいたい「このマスにこの数字を入れるか否か」とか、「この辺に線を引くかどうか」とか、「このマスを塗るかどうか」、とか、そういうのを決定する問題といえます。それってさっき言ってた論理変数そのものですよね。
だから、マスや辺ごとに論理変数を用意して、制約を論理式として書き下し、それを SAT ソルバーくんに投げれば、SAT ソルバーくんが勝手に解いてくれる、ないし解があるかを判定してくれるわけです！やったね！
ちなみにおまじないですが、ペンシルパズルはだいたい NP で、SAT は NP 完全なので、ペンシルパズルを SAT に還元できることは保証されているようです。なんで、ペンシルパズルはだいたい SAT ソルバーくんに投げれば解いてくれるんだな！ガッハッハ！(よくわかってない人のつぶやき)
解く際の困難
はい、そんなに甘くありません。
まずは単純に、論理式を書くのがダルいということ。これについては、Sugar という、制約を書きやすくする言語を使えばそれなりに解決しますが、それでも全部書き下すのは大変な場合が多いです。10*10 だと変数 100 個だし。なので今ぼくは、
制約を Sugar の言語を用いて紙に書き出す→ Python でそれらの式を生成するコードを書く → (ここまで人間の仕事) → Python が Sugar の式を生成する → Sugar に投げると SAT を生成する → SAT ソルバー君がそれを解く
ということをしています。いったい何をやっているんだ... せめて for 文くらい使えないのかなぁ。
次に、実行時間の問題。「解ける」と言っても、ここから 7638 年かかるとか言われたら意味ないですよね。これについては、サイズが大きいのはさすがに諦めるというのと、ある程度高速に動いてくれるように論理式を工夫してやる必要があります。
今のところ、ルールや入力する問題にもよりますが、サイズ 10 ぐらいがちょうど限界かなぁという印象です。ぼくの頑張りが足りないだけかも...
さらにそもそも制約を書き下せるかという問題。SAT に落とし込む際の相性があるっぽいです。具体的には、数字埋め系・配置系などはかんたん、ループ・(連結性のある) 塗るパズルはむずかしい。つまり全体制約を書き下すのが大変です。さらに、なんとか書き下したとしても、変数が増えると実行時間も膨大に増えます。困る。
なので、SATソルバーくんはペンシルパズルを解く上で、 (NP 完全と言う意味で) 万能であるが、(実行時間や手間の面で) 万能ではない、という印象です。
作ったもの
・魔法陣が解けると書いてあったので、ソルバーを書いて遊んだ。
サイズ 3 だと面白くないと思い、サイズ 5 で作った。魔法陣の制約ってサイズが大きくなるとゆるゆるなので、その後いろいろ制約を与えて遊んでいた。
その中で、「四隅の和の最小は 26」ということがわかった。これは愚直に投げても SAT ソルバーくんはすぐには答えを返してくれず、理由を考察しているうちに数学的な制約に気付き、数学的に解けてしまった。その後、その証明で使った不等式評価を追加したら、ソルバーくんもすぐに答えを返してきた。
この経験より、「ソルバーくん、人間のわかる制約とかあんまり考えずに探索しちゃうので、使えそうな評価は手筋は搭載してもいいかもね」という気付きを得た。
・わんどさん (@wand_125) のつくった「シンプルガコ」というパズルのソルバーを書いた。これはジャンルが数字埋めで、かなり愚直に書けるなと思ったため。ちなみにルール自体は単純だが、わりと人間が解くのはつらめなパズルではある...(まだ手筋開発がされてないだけかもしれないが)。また、たしかサイズが 7 以下なら一瞬で解けて、サイズ 9 くらいでもそれなりの時間で解ける。
なお Python の利用により、問題をテキストに入力するだけで、論理式を生成し (半) 自動で解いてくれるようにした。いままで他の人の作ったソルバーを使ってきたときみたいな感じで動くので、それがなんかうれしかった。ただし情報の知識に乏しいため公開ができない...
あと、同じ作戦を使えばシンプルガコの元ネタである「ガコ」のソルバーも書けるとわかった。が、同じことなのでまだ試していない。ペンパ業界では有名な (悪名高き？) 「ガコ2」という激ヤバパズルがあって、それはたしかサイズ 10 だが、それなりの時間で解いてくれるかは不明 (シンプルガコに比べ、変数 2 倍なので)。
・Sugar でペンパを解く説明スライドに沿って、へやわけの最密充填を求めるソルバーを書いた。これは「いくつか黒マスを隣り合わないように配置し、白マス連結のままたくさん置きたい」というもの。普通の最密充填と違い、四方の辺を考慮している。
「白マスひとつながり」を表現するのが大変だが、これについてスライドの方法を使った。作戦は「白マスのつながりに対応して根付き木をつくり、根が 1 個であることを確認する」というもの。これなら、黒マスを表す変数に加え、つながり方をカウントする変数と根を表す変数を用意すれば解ける。詳しくはスライド参照。
実際に実装したところ、盤面のマス数が 50 個ぐらいを境に、急激に解いてくれなくなった。変数が多く、無駄な探索に時間をかけている説がある。「インクリメンタル SAT」なるものがあるらしく、これはざっくり「無駄な探索をしないよう、成立しない真偽の組み合わせを論理式として順々に追加する」というものらしい。SAT ソルバーの性能向上のための技術らしいが、一般公開されてるかあやしい。使ってみたいぞー (環境構築でまた地獄を見そうだが...)
感想
ペンパ側からみた感想がちょっとあるのですが、おいおい書きます...
参考文献・サイト
いろいろ見て、いろいろまねて (パクって) ますが、すんません、これもあとでまとめます...
ヘルプミー
読めばわかる通り、めっちゃ手探りでやってるし、理解もあやしいです。「これいいぞ」とか「これはアカンぞ」とかあったらガンガン教えてください。助けの求め方が雑ゥ！
