制約充足問題
函館で開催されたFUN-AIというAI（人工知能）関係の研究会に参加。
最初の発表「パズルのためのプログラミング言語」で紹介された制約充足問題を各種プログラミング言語を用いて解く話が面白かったです。
数独の問題も制約条件をきちんと定義すればソルバですぐに解けるという話で、
そういえば、タイムインターメディアの藤原さんも同じテーマの内容をWebで書いていたことを思い出しました。
さっそく検索して、こちらのページを発見。
まさに数独の問題を制約ソルバーで解いてしまおうというものです。
自分でプログラミングしないでも、ルールを教えてあげれば答えが出てくるということがとても面白いです。
どうやら、意外と簡単にルールを記述できるっぽいので、自分でも実験してみることにしました。
まずは、制約ソルバーを準備することから。どうやらSugarというものが有名らしいので、これをインストールしてみます。
と、思い立ったのはいいものの、JDK,Perl,minsat,sugarが必要で、動作させるまでに苦労してしまいました。
基本的には、こちらの解説に素直に従えばよいはずなのですが、そうはいかず。。
結局、Cygwin版のminsatが正しく動作しないのが原因で、自分でmakeすることで解決しました。
ただ、Cygwinのデフォルトの設定ではmakeがインストールされていないので、まずはmakeを自分で追加インストールする必要があります。
で、さっそく何か問題を解いてみよう！
ということで、何か適切な問題がないか考えたところ、今回の羽田→函館間の飛行機の中で読んだ雑誌にあった問題を思い出して、それにチャレンジすることにしました。
問題は、確かこんな感じ。
・A,B,C,Dの4人が橋を渡って反対側に行きたい。
・片道を渡るのに、Aは1分、Bは2分、Cは5分、Dは10分かかる。帰りも同じだけかかる。
・橋を渡れるのは一度に2人だけ。必ず懐中電灯を持ってわたる必要があるが、懐中電灯は1つだけ。
・橋は17分後に壊れてしまう。無事に全員が渡るにはどうすればよいか。
で、雑誌に載っていた答えは次のような感じ。
AとBが一緒に渡る(2分)
Aが戻ってくる(1分)
CとDが一緒に渡る(10分)
Bが戻ってくる(2分)
AとBが一緒に渡る(2分)
で、合計17分
なるほどなるほど、なかなか面白い問題です。
で、この問題を制約式として表現できればよいということになります。
まぁ、詳しいことはさておき、次のような式を作ってみました。
（生まれて初めての制約プログラミング。たぶん、もっとスマートに書けるのでしょうが、最初はこんなもんでご勘弁）
考え方：行きで1ターン、帰りで1ターン、という具合にカウントすると、全部で5ターンで全員が渡り終えるはず。
nターンめで、渡る場合を1、戻ってくる場合を-1、何もしない場合を0とし、それぞれ、an,bn,cn,dnと表わす。
(int a1 0 1)(int a2 -1 0)(int a3 0 1)(int a4 -1 0)(int a5 0 1)
(int b1 0 1)(int b2 -1 0)(int b3 0 1)(int b4 -1 0)(int b5 0 1)
(int c1 0 1)(int c2 -1 0)(int c3 0 1)(int c4 -1 0)(int c5 0 1)
(int d1 0 1)(int d2 -1 0)(int d3 0 1)(int d4 -1 0)(int d5 0 1)
(= (+ a1 b1 c1 d1) 2) ; 1ターンめでは2人が渡る
(= (+ a2 b2 c2 d2) -1) ; 2ターンめでは1人が戻ってくる
(= (+ a3 b3 c3 d3) 2) ; 3ターンめでは2人が渡る
(= (+ a4 b4 c4 d4) -1) ; 4ターンめでは1人が戻ってくる
(= (+ a5 b5 c5 d5) 2) ; 5ターンめでは2人が渡る
; 値は0か1かのどちらか
(or (= (+ a1 a2) 0) (= (+ a1 a2) 1))
(or (= (+ b1 b2) 0) (= (+ b1 b2) 1))
(or (= (+ c1 c2) 0) (= (+ c1 c2) 1))
(or (= (+ d1 d2) 0) (= (+ d1 d2) 1))
(or (= (+ a1 a2 a3) 0) (= (+ a1 a2 a3) 1))
(or (= (+ b1 b2 b3) 0) (= (+ b1 b2 b3) 1))
(or (= (+ c1 c2 c3) 0) (= (+ c1 c2 c3) 1))
(or (= (+ d1 d2 d3) 0) (= (+ d1 d2 d3) 1))
(or (= (+ a1 a2 a3 a4) 0) (= (+ a1 a2 a3 a4) 1))
(or (= (+ b1 b2 b3 b4) 0) (= (+ b1 b2 b3 b4) 1))
(or (= (+ c1 c2 c3 c4) 0) (= (+ c1 c2 c3 c4) 1))
(or (= (+ d1 d2 d3 d4) 0) (= (+ d1 d2 d3 d4) 1))
(= (+ a1 a2 a3 a4 a5) 1) ; Aは最終的には渡り終わる
(= (+ b1 b2 b3 b4 b5) 1) ; Bは最終的には渡り終わる
(= (+ c1 c2 c3 c4 c5) 1) ; Cは最終的には渡り終わる
(= (+ d1 d2 d3 d4 d5) 1) ; Dは最終的には渡り終わる; 以下、最も時間のかかる人に合わせて移動して、合計が17分に納まるという制約
(le (+
(max (if (= d1 1) 10 0)
(max (if (= c1 1) 5 0)
(max (if (= b1 1) 2 0)
(if (= a1 1) 1 0)
)
)
)
(max (if (= d2 -1) 10 0)
(max (if (= c2 -1) 5 0)
(max (if (= b2 -1) 2 0)
(if (= a2 -1) 1 0)
)
)
)
(max (if (= d3 1) 10 0)
(max (if (= c3 1) 5 0)
(max (if (= b3 1) 2 0)
(if (= a3 1) 1 0)
)
)
)
(max (if (= d4 -1) 10 0)
(max (if (= c4 -1) 5 0)
(max (if (= b4 -1) 2 0)
(if (= a4 -1) 1 0)
)
)
)
(max (if (= d5 1) 10 0)
(max (if (= c5 1) 5 0)
(max (if (= b5 1) 2 0)
(if (= a5 1) 1 0)
)
)
)
)
17
)
で、出てきた答えは次の通り。
s SATISFIABLE
a a1 1
a a2 0
a a3 0
a a4 -1
a a5 1
a b1 1
a b2 -1
a b3 0
a b4 0
a b5 1
a c1 0
a c2 0
a c3 1
a c4 0
a c5 0
a d1 0
a d2 0
a d3 1
a d4 0
a d5 0
a
これを実際の動きに当てはめると、
AとBが一緒に渡る(2分)
Bが戻ってくる(2分)
CとDが一緒に渡る(10分)
Aが戻ってくる(1分)
AとBが一緒に渡る(2分)
で、合計17分
むむむ、、良く見ると雑誌に載っていた答えと違いますが、確かに条件を満たしています。
なんと、偶然にも別解を見つけてしまったらしいです。
考えてみれば簡単な問題ですが、コンピュータに解かせることで新しい解を発見できたということは、とても面白いなぁ。
ちなみに、最後の「17分」という制約を「16分」に変更すると
s UNSATISFIABLE
となって、16分以下の答えは存在しないことがわかります。
初めてのSugar手習い、ということで大変よい勉強になりました。
