ブログのとさか

技術的な話をしたりしなかったり

SuperCon 2016 予選問題をCSPソルバーで解く

SuperCon 2016 参加者の皆さん予選お疲れ様でした。予選通過するといいですね。 僕は高校生で無くなってしまったので本戦への参加権はありませんが、予選問題を読んだところCSPソルバーでさくっと解けそうだったのでやってみました。

※この記事はしっかりとした解説記事ではなく、紹介程度のものです。

CSPソルバーとは

CSPソルバーとは、問題の制約を決まった形式のテキストに変換し、そのファイルをCSPソルバーに渡して上げると、内部で「いい感じ」に問題を解いてくれるというツールです。予選参加者のみなさんは頑張って探索を最適化していったと思いますが、CSPソルバーを使うと簡単なテキストファイルを生成するだけでそれなりに高速に問題を解いてくれます。（とは言ってもみなさんのガチガチにチューニングしたプログラムの方がだいぶ速いと思います。）

CSPソルバーで虫喰い魔方陣を解く

百聞は一見にしかず。CSPソルバーについての詳しい説明は横において、今回の問題を解く様子を見てみましょう。CSPソルバーにはSugarを使います。
とはいっても、魔方陣の解法については自分が書くことはあまりなく、「CSPソルバー 魔方陣」で検索すると

http://bach.istc.kobe-u.ac.jp/sugar/puzzles/sugar-puzzles.pdf

というスライドのPDFが引っ掛かり、このスライドにある3×3魔方陣のCSPファイルと同じように6×6用のCSPファイルを生成するだけで解くことができます。

具体的には以下のようになります。

;それぞれの魔方陣のマスに入る数をx_i_jという変数で表す
(int x_0_0 1 36);整数変数 x_0_0 の宣言。範囲は 1 <= x_0_0 <= 36 となる。
(int x_0_1 1 36)
(int x_0_2 1 36)
(int x_0_3 1 36)
(int x_0_4 1 36)
(int x_0_5 1 36)
(int x_1_0 1 36)
(int x_1_1 1 36)
(int x_1_2 1 36)
(int x_1_3 1 36)
(int x_1_4 1 36)
(int x_1_5 1 36)
(int x_2_0 1 36)
(int x_2_1 1 36)
(int x_2_2 1 36)
(int x_2_3 1 36)
(int x_2_4 1 36)
(int x_2_5 1 36)
(int x_3_0 1 36)
(int x_3_1 1 36)
(int x_3_2 1 36)
(int x_3_3 1 36)
(int x_3_4 1 36)
(int x_3_5 1 36)
(int x_4_0 1 36)
(int x_4_1 1 36)
(int x_4_2 1 36)
(int x_4_3 1 36)
(int x_4_4 1 36)
(int x_4_5 1 36)
(int x_5_0 1 36)
(int x_5_1 1 36)
(int x_5_2 1 36)
(int x_5_3 1 36)
(int x_5_4 1 36)
(int x_5_5 1 36)

; すべての変数は互いに違う数を取る
(alldifferent x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_0_5 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_1_5 x_2_0 x_2_1 x_2_2 x_2_3 x_2_4 x_2_5 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_3_5 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 x_4_5 x_5_0 x_5_1 x_5_2 x_5_3 x_5_4 x_5_5)

;縦、横、対角線のマスに入る数の和が111になる（ポーランド記法で書く）
(= 111 (+ x_0_5 (+ x_0_4 (+ x_0_3 (+ x_0_2 (+ x_0_1 x_0_0))))))
(= 111 (+ x_1_5 (+ x_1_4 (+ x_1_3 (+ x_1_2 (+ x_1_1 x_1_0))))))
(= 111 (+ x_2_5 (+ x_2_4 (+ x_2_3 (+ x_2_2 (+ x_2_1 x_2_0))))))
(= 111 (+ x_3_5 (+ x_3_4 (+ x_3_3 (+ x_3_2 (+ x_3_1 x_3_0))))))
(= 111 (+ x_4_5 (+ x_4_4 (+ x_4_3 (+ x_4_2 (+ x_4_1 x_4_0))))))
(= 111 (+ x_5_5 (+ x_5_4 (+ x_5_3 (+ x_5_2 (+ x_5_1 x_5_0))))))
(= 111 (+ x_5_0 (+ x_4_0 (+ x_3_0 (+ x_2_0 (+ x_1_0 x_0_0))))))
(= 111 (+ x_5_1 (+ x_4_1 (+ x_3_1 (+ x_2_1 (+ x_1_1 x_0_1))))))
(= 111 (+ x_5_2 (+ x_4_2 (+ x_3_2 (+ x_2_2 (+ x_1_2 x_0_2))))))
(= 111 (+ x_5_3 (+ x_4_3 (+ x_3_3 (+ x_2_3 (+ x_1_3 x_0_3))))))
(= 111 (+ x_5_4 (+ x_4_4 (+ x_3_4 (+ x_2_4 (+ x_1_4 x_0_4))))))
(= 111 (+ x_5_5 (+ x_4_5 (+ x_3_5 (+ x_2_5 (+ x_1_5 x_0_5))))))
(= 111 (+ x_5_5 (+ x_4_4 (+ x_3_3 (+ x_2_2 (+ x_1_1 x_0_0))))))
(= 111 (+ x_5_0 (+ x_4_1 (+ x_3_2 (+ x_2_3 (+ x_1_4 x_0_5))))))

ただし、このCSPファイルはすべての魔方陣のマスが開いている状態の制約を表しているので、既に埋まっている場所は制約として追記して上げる必要があります。 例えば次の魔方陣の場合、
18 13 35
20 33 19 7
2 32 10 9
30 3 15
29 4 26 28
5 31 16

以下の様に制約を追記します。

(= x_0_1 18)
(= x_0_3 13)
(= x_0_4 35)
(= x_1_1 20)
(= x_1_2 33)
(= x_1_3 19)
(= x_1_4 7)
(= x_2_1 2)
(= x_2_2 32)
(= x_2_4 10)
(= x_2_5 9)
(= x_3_0 30)
(= x_3_3 3)
(= x_3_5 15)
(= x_4_1 29)
(= x_4_2 4)
(= x_4_4 26)
(= x_4_5 28)
(= x_5_2 5)
(= x_5_3 31)
(= x_5_4 16)

あとはこのファイルを適当な名前(ここではmahou.cspとします)で保存し、sugarに渡すだけです。

% sugar mahou.csp
s SATISFIABLE
a x_0_0 6
a x_0_1 18
a x_0_2 25
a x_0_3 13
a x_0_4 35
a x_0_5 14
a x_1_0 11
a x_1_1 20
a x_1_2 33
a x_1_3 19
a x_1_4 7
a x_1_5 21
a x_2_0 36
a x_2_1 2
a x_2_2 32
a x_2_3 22
a x_2_4 10
a x_2_5 9
a x_3_0 30
a x_3_1 34
a x_3_2 12
a x_3_3 3
a x_3_4 17
a x_3_5 15
a x_4_0 1
a x_4_1 29
a x_4_2 4
a x_4_3 23
a x_4_4 26
a x_4_5 28
a x_5_0 27
a x_5_1 8
a x_5_2 5
a x_5_3 31
a x_5_4 16
a x_5_5 24
a

この通りに埋めると
6 18 25 13 35 14
11 20 33 19 7 21
36 2 32 22 10 9
30 34 12 3 17 15
1 29 4 23 26 28
27 8 5 31 16 24

となり、確かに解けていることが分かります。（すごい！）

実行時間をtimeコマンドで計測すると

real 0.94
user 0.46
sys 0.47

となりました。まぁまぁですかね。実行環境はVirtualBox上のUbuntu（メモリ1GB、CPU Core i7-6650U 2.20GHz）、内部で使用しているSATソルバーはMinisatです。
最悪ケースでどうなるかは自分も確かめてないので試してみてください。

このように、CSPソルバーを使うと問題の解が簡単に得られます。もちろん魔方陣以外にも様々な問題を解くことができます。
SuperConのような単一のソースファイルを提出するコンテストではこれをそのまま回答コードとして流用するのは難しいですが、覚えておくとテストケース生成の際などに役立つかもしれません。

参考

ひとりごと

本当は魔方陣のルールをdirect encodingとorder encodingで表すプログラムをそれぞれ書いて比較するっていうテーマにして、Sugarはついでで紹介するだけみたいなブログ記事にする予定だったけど、ちょっと時間が取れ無さそうだったのでとりあえずSugarの紹介だけすることにしました...
あと本当はWindows上でSugarを動作させたかったけど、うまく行かなかったので後回し中。でも大体原因がわかった（と思う）ので、もしできたらそれについてのブログも書くかも...？
SuperCon、現役としてもう一回やりたかったなあ。