皆さんこんにちは！53代のshiro(@shiro537)と申します。
趣味は競技プログラミング・アニメ鑑賞・読書です。
一応プログラミング研究会に所属しています。
新歓ブログリレー11日目ということで、今日は(ニコリの)ペンシルパズルをパソコンで解く話をしたいと思います。
はじめに
ペンシルパズルとは？
ペンシルパズル（pencil puzzle）とは、図示された問題に対して答えを徐々に書き込むことによって、最終的な解答を行う形式のパズルのことである。 リトゥンパズル（written puzzle）とも呼ばれる。
現在はパズルの専門雑誌がいくつも存在し、以下のパズルのいずれか一種類専門の雑誌も多い。パズルの形式（種類）自体に新しいものが次々と考え出されているが、それらの種類の名称は必ずしも共通しておらず、雑誌（出版社）により異なる場合がある。
だそうです。要するに雑誌の懸賞とかでお母さんが応募してたり旅行のお供になったりしがちな、アレです。
SATとは
SATとはSATisfiabilityの略で「充足可能性問題」とも呼ばれ、「乗法標準形(CNF)で表された論理式をtrueにするような変数の割り当て方が存在するかどうか、存在するならその割り当て方を1つ出力しなさい」という問題のことで、NP完全として知られています。(情報理工学科だと、2年秋学期の情報数学Bで習った)
SATソルバーとは、これを解くプログラムのことを言います。
Sugar制約ソルバー
では、SATソルバーでパズルを解くにはどうすればよいのでしょうか？
まさかパズルをそのまま与えるわけにもいきません。
SATソルバーで問題を解くには、「SATソルバーで解ける形にする」必要があります。
つまり...
- 問題を乗法標準形の論理式に変換して
- SATソルバに入力として与えて
- 出力として得た変数の割り当てを問題の解に変換する
という手順を踏む必要があるようです。
筆者は最初これを作ろうとしたんですが、色々調べたところSATソルバーの歴史はかなり深く、SATソルバーの性能を競うコンペなんてのもあるらしい。昔は研究室単位でこれを作ったりしたとかなんとか。当然作るのは大変です。
プレパラートより脆い筆者の心はすぐに折れてしまいました。
しかし、一般に優秀なSATソルバーは公開されていることが多いことも知りました。その中の1つがSugar制約ソルバーというものです。
これはどういうものかというと、
- 問題の制約を.cspという独自の拡張子を持ったファイルに記述する
- sugarに投げる
- 解が存在するかどうかを判定し， 解が存在すればその解を表示される
- ＼＼\ ٩( ‘ω’ )و //／／ ｳﾚｼｲ!!!
というものです。すごい...（厳密にはMiniSatというSATソルバーを用いて、制約充足問題 (CSP) をSAT問題に変換して解くものだそうです）
なんだか難しそうですが、要するに、
ルールを適切に記述してあげるだけで、Sugarが勝手に解いてくれる
ということです。
では、どのように使うのでしょうか。次に使い方を説明していきたいと思います。
Sugarの導入方法
導入にはHomebrewを用いました。
環境
Sugarのインストール
- Sugar公式から最新のzipファイル(v2-3-3)をインストールします。
- 次に、パスを通します。自分はターミナルで
$ vi ~/.bash_profile
- と入力し、次の内容を追記して、
export PATH="/Users/(ユーザーネーム)/Desktop/sugar-v2-3-3/bin/sugar:$PATH"
- .bash_profileを読み込みました。
$ source ~/.bash_profile
ターミナルで
sugarと入力し、なんか色々説明が出力されたらOKです。
こんな感じのがバーっと出てきたら成功 次にminisatをインストールします...といいたいのですが
$ brew install minisatとするとどうしてもnot foundと言われてどうしようもなかったので、代わりにcryptominisatというやつを使うことにしました。ターミナルで以下の文を打つだけでOKです。
$ brew install cryptominisat
よくわかんないけどhomebrewすげー
- 最後にSugarの環境設定をします。適当なテキストエディタでsugar-v2-3-3/sugar/bin 内のこの部分を次のように修正しましょう。
my $version = "v2-3-3"; my $java = "java"; my $jar = "/Users/(ユーザーネーム)/Desktop/sugar-$version/bin/sugar-$version.jar"; my $solver0 = (cryptominisatのあるパスを書く); my $solver0_inc = "minisat-inc"; my $tmp = "/Users/(ユーザーネーム)/Desktop/sugar-$version/tmp_sugar/sugar$$";
- 修正したら保存して、examplesディレクトリに移動し、次のコマンドを入力します。
$ sugar nqueens-8.csp
これはどうやら、有名な8クイーン問題の制約が記述された.cspファイルのようです。正しく環境構築できていればなんらかの解がこのように出力されるはずです。
実際にパズルを解いてみる
今回は9*9の数独を解いてみましょう。
なぜ数独かというと、数独はルールが簡単で、制約を記述するのが楽だからです。
数独のルール
ニコリより引用。(https://www.nikoli.co.jp/ja/puzzles/sudoku/)
- まだ数字の入っていないマスに１から９までの数字のどれかを１つずつ入れましょう。０(ゼロ)は使いません。
- タテ列（９列あります)､ヨコ列（９列あります)､太線で囲まれた３×３のブロック（９つあります）のどれにも、１から９までの数字が１> つずつ入るようにします。
cspファイルの記述の仕方
上のルールをcspファイルに記述していきます。詳しい文法は公式ドキュメント(英語)を参考にして下さい。
ルール1
まず、「各マスに1~9の整数のうちどれかが入る」というルールを表現します。
- 各マスにつき1〜9の数字を取る変数を割り当てます。つまり、i行j列のマスに変数x_i_j(0-indexed)を割り当てます。
- 1つの変数につき、以下のように宣言します。例えば0行0列目が空マスだった場合、
(int x_0_0 1 9) ; 0行0列目には1~9のどれかが入る
- という風に1行に書きます。また、例えば2行3列目に1が入ることが既に確定している場合は、
(int x_2_3 1 1) ; 2行3列目には1が入る
- という風に1行に書きます。
;はコメントです。
ルール2
次に、「タテ、ヨコ、3*3のブロックに1~9の数字が1つずつ入る」という制約を追記します。
- 例えば0行目の場合、
; 0行目には、1~9の整数が1つずつ入る。重複してはいけない。 (allDifferent x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_0_5 x_0_6 x_0_7 x_0_8)
- という風に1行に書きます。他の行や列、ブロックについても同様に書いていきます。
適当に自動化
これを手で書くのは非常に面倒なので、Pythonで適当にスクリプトを書きました。
具体的には、in.txtのような形式から入力を受け取り、suudoku-9-9.cspに書き込むだけです。(0は空きマスを表しています。詳しい説明はREADMEに。)
$ sugar suudoku-9-9.csp
とターミナルでコマンドを打つと、こんな感じで答えが返ってきます。
テキストに直すとこんな感じで、ざっと見た感じ正解の出力が得られていることがわかりました。
5 3 6 8 2 7 9 4 1 1 7 2 9 6 4 3 5 8 8 9 4 1 5 3 2 6 7 7 1 5 3 4 9 8 2 6 6 4 3 7 8 2 1 9 5 9 2 8 5 1 6 7 3 4 4 8 1 2 9 5 6 7 3 3 6 9 4 7 1 5 8 2 2 5 7 6 3 8 4 1 9
まとめ
数独だけでなく、様々なニコリのパズルがSugarで解けるようです。詳しくはこのサイトを見て下さい。自分も本記事を格上で大いに参考にさせて頂きました。
自分が今一番ハマっているペンシルパズルはヤジリンというのですが、これも制約を適切に記述することでSugarで解けるらしいです。ただパズルの種類によっては制約の記述が大変だったりするようです。
今回は時間があまりなかったので、簡単な数独を紹介させて頂きました。今度はヤジリンも書いてみたいなあと思ってます。
ここまで長い文章を読んで頂き大変感謝です。ありがとうございました！
明日は53代ナカト君の記事です。お楽しみに。