Sugarという制約ソルバーがあります。
開発元である田村先生のページで、ニコリのいろいろなパズルをSugarで解く試みが発表されています。
また、藤原博文さんは田村先生のページで発表されている以外のパズルをSugarで解く試みを発表されています。
さらに当ブログでも、ひとりにしてくれの穴埋めを行ったり、スケルトンを解いた記事を上げています。解けたんじゃないかな。
以上を踏まえて今回は、カナオレをSugarを使って解いてみようと思います。
いきなり普通サイズの問題に取り組むのは、いろいろ不都合が起きた場合に原因が見つかりにくくなりがちです。ということでまずはごく小さな例題から取り組むことにしましょう。３ｘ３の例題です。
目でも解けるくらいですね。
ここで注意しますが、現在、ぼくはこの小さな問題でしか試験を行っていません。なので、以下延々書くことは大嘘かもしれませんのでご注意下さい。まあその辺は自分で検証するのが知恵で世界に立ち向かう態度だ！
それはともかく。
これはこれで良いのですが、どうもアルファベットを使用するとカナオレを解いている気がしないというリクエストにお応えして、あくまでランダムに、かなを対応させてみることにします。
あくまでランダムですが、えらいもので、これでずいぶん解りやすくなりましたね。
さて、この３ｘ３の盤面に、次のように座標、および名前を振ります。
おわかりでしょうか。たとえば、Ｘ座標１、Ｙ座標２のマスには「７」という名前がついています。また、「２」という名前がついたマスのＸ座標は２、Ｙ座標は０になります。できるなら０１２３４５６７８の代わりにＡＢＣＤＥＦＧＨＩとかの名前をつけた方が良いかと思うのですが、Sugarで扱うには今のところ数字の方が都合が良いのでご了承ください。
さて、カナオレの各単語の各文字に対して、以下のような変数を定義します。インデックスは0から開始してますのでご注意を。
W_n_m_X -> n番目の単語のm番目の文字のＸ座標
W_n_m_Y -> n番目の単語のm番目の文字のＹ座標
W_n_m -> n番目の単語のm番目の文字の入るマスの名前
本質的には最後の変数群は必要ないのでしょうが、この方が解りやすいと思うので導入しました。WはWordの頭文字という以上の意味はありません。今回の問題に適用するとこうなります。
ここで、今回の盤面では、W_n_m_XとW_n_m_Yは0,1,2の整数、W_n_mは0から8までの整数になります。このことをSugarでは以下のように書きます。
(int W_0_0_X 0 2) (int W_0_0_Y 0 2) (int W_0_1_X 0 2) ...【中略】... (int W_2_3_Y 0 2) (int W_2_4_X 0 2) (int W_2_4_Y 0 2) ...【中略】... (int W_2_2 0 8) (int W_2_3 0 8) (int W_2_4 0 8)
さてここで、ＸＹ座標と名前を１対１に対応させる式を考えます。次のようになりますね。
W_n_m = W_n_m_Y × ３ ＋ W_n_m_X
X軸の項目数３を変えれば、この式は一般に使うことができます。Sugarでは次のように表現します。
(= W_0_0 ( + (* W_0_0_Y 3) W_0_0_X) ) (= W_0_1 ( + (* W_0_1_Y 3) W_0_1_X) ) (= W_0_2 ( + (* W_0_2_Y 3) W_0_2_X) ) (= W_1_0 ( + (* W_1_0_Y 3) W_1_0_X) ) (= W_1_1 ( + (* W_1_1_Y 3) W_1_1_X) ) (= W_1_2 ( + (* W_1_2_Y 3) W_1_2_X) ) (= W_2_0 ( + (* W_2_0_Y 3) W_2_0_X) ) (= W_2_1 ( + (* W_2_1_Y 3) W_2_1_X) ) (= W_2_2 ( + (* W_2_2_Y 3) W_2_2_X) ) (= W_2_3 ( + (* W_2_3_Y 3) W_2_3_X) ) (= W_2_4 ( + (* W_2_4_Y 3) W_2_4_X) )
さらに、カナオレでは１文字目、２文字目の入る場所は確定しているので、W_0_m_X、W_1_m_X、W_0_m_Y、W_1_m_Y、W_0_m、W_1_m、は確定します。今回の問題について表を埋めてみましょう。以下のようになったでしょうか。
これもSugarの表現に落としてみます。上で座標と名前を対応させたので、座標だけでかまいません。名前だけでももちろんかまいませんが、あとあと面倒かと思います。
(= W_0_0_X 0) (= W_0_0_Y 1) (= W_0_1_X 0) (= W_0_1_Y 0) (= W_1_0_X 1) (= W_1_0_Y 2) (= W_1_1_X 1) (= W_1_1_Y 1) (= W_2_0_X 2) (= W_2_0_Y 0) (= W_2_1_X 2) (= W_2_1_Y 1)
次は文字のつながりを考えます。カナオレのルールから、n番目の単語のm番目の文字とn番目の単語のm+1番目の文字はタテヨコに隣り合っています。これを数式で書くと、
「W_n_m_X=W_n_(m+1)_X かつ W_n_m_Y - W_n_(m+1)_Y = 1」であるか、
「W_n_m_X=W_n_(m+1)_X かつ W_n_(m+1)_Y - W_n_m_Y = 1」であるか、
「W_n_m_Y=W_n_(m+1)_Y かつ W_n_m_X - W_n_(m+1)_X = 1」であるか、
「W_n_m_Y=W_n_(m+1)_Y かつ W_n_(m+1)_X - W_n_m_X = 1」である。
ということになります。ちなみに、上から、「文字が下に進む」「文字が上に進む」「文字が左に進む」「文字が右に進む」に対応します。
この問題での、「たむら」の「む」→「ら」の場合を書き下してみましょう。
(|| (&& ( = W_0_1_X W_0_2_X) (= (- W_0_1_Y W_0_2_Y) 1) ) (&& ( = W_0_1_X W_0_2_X) (= (- W_0_2_Y W_0_1_Y) 1) ) (&& ( = W_0_1_Y W_0_2_Y) (= (- W_0_1_X W_0_2_X) 1) ) (&& ( = W_0_1_Y W_0_2_Y) (= (- W_0_2_X W_0_1_X) 1) ) )
他の文字のつながりについても同様に記述します。枠外に出る場合も表現できてしまいますが、それは座標の範囲を0,1,2に区切ってあるので除外されます。また、「もと来た方向に戻る」は禁じられているので、条件は４種類ではなく３種類で済むはずですが、個々に対応するのは面倒なので後で除外します。ここで３種類に絞りたい方はそう書いても問題ないです。その方が速くなるかも。
さあ、最後は文字の重なりを表現しましょう。カナオレのルールから、違う文字は同じ名前のマスには入りません。同じ文字は同じ名前のマスに入るかもしれません。（し、入らないかもしれません）
今回の問題では「ゆかり」の「ゆ」と「ほりえゆい」の「ゆ」が、また、「ゆかり」の「り」と「ほりえゆい」の「り」が同じ文字となっています。それ以外は違う文字になります。「ゆ」として「ゆかり」の「ゆ」、「り」として「ゆかり」の「り」を採用すると、
『W_0_0,W_0_1,W_0_2,W_1_0,W_1_1,W_1_2,W_2_0,W_2_2,W_2_4は全部異なる』
となります。「ゆ」の字が２つ、「り」の字が２つありますから、２×２＝４本の条件が必要になります。この問題ではたった４本ですが、大きくすると多分ここがえらく泥臭くなるはず。
また、今回の例題にはありませんが、ひとつの単語の中に同じ文字が２回以上出てくる場合も、ここの条件に織り込んで除外します。
Sugarには「全部違う」という式が用意されていて、以下のように書けます。
(alldifferent W_0_0 W_0_1 W_0_2 W_1_1 W_2_0 W_2_1 W_2_2 W_2_3 W_2_4) (alldifferent W_0_0 W_0_1 W_0_2 W_1_1 W_1_2 W_2_0 W_2_2 W_2_3 W_2_4) (alldifferent W_0_0 W_0_1 W_0_2 W_1_0 W_1_1 W_2_0 W_2_1 W_2_2 W_2_4) (alldifferent W_0_0 W_0_1 W_0_2 W_1_0 W_1_1 W_1_2 W_2_0 W_2_2 W_2_4)
さてこれで、カナオレの条件はすべて列挙できたはずです。さっそくsugarに食わせてみましょう。ぼくの環境では数秒で答えが出ました。
s SATISFIABLE a W_0_0_X 0 a W_0_0_Y 1 a W_0_1_X 0 a W_0_1_Y 0 a W_0_2_X 1 a W_0_2_Y 0 a W_1_0_X 1 a W_1_0_Y 2 a W_1_1_X 1 a W_1_1_Y 1 a W_1_2_X 2 a W_1_2_Y 1 a W_2_0_X 2 a W_2_0_Y 0 a W_2_1_X 2 a W_2_1_Y 1 a W_2_2_X 2 a W_2_2_Y 2 a W_2_3_X 1 a W_2_3_Y 2 a W_2_4_X 0 a W_2_4_Y 2 a W_0_0 3 a W_0_1 0 a W_0_2 1 a W_1_0 7 a W_1_1 4 a W_1_2 5 a W_2_0 2 a W_2_1 5 a W_2_2 8 a W_2_3 7 a W_2_4 6 a
ちゃんと答えになっているのが確認できましたか？
じゃあ、大きくしてみてもちゃんと解けるのかな？ というのが自然な疑問になりますが、先生もうちょっと疲れてしまいました。それは次回以降に扱うことにします。もちろん自主的に演習してきても構いませんよ。
それでは、今日の講義はこれでおしまいにします。（ぺこり）
