Sugarという制約ソルバーがあります。
開発元である田村先生のページで、ニコリのいろいろなパズルをSugarで解く試みが発表されています。
また、藤原博文さんは田村先生のページで発表されている以外のパズルをSugarで解く試みを発表されています。
さらに当ブログでも、ひとりにしてくれの穴埋めを行ったり、スケルトンを解いたり、カナオレを解いたり、変則シークワーズを作ったりする記事を上げています。上げたんじゃないかな。
以上を踏まえて今回は、推理パズルをSugarを使って解いてみようと思います。
ニコリの推理パズルの紹介ページはこちら。
また今回、「簡易推理ロジック」というソフトウェアをもろもろ使用させていただいています。（ページ下部にリンクがあります）
トップページから辿る方がお行儀が良いかもしれません。
例題は以下。この例題はフィクションであり、実在のアニメ漫画等の作品、天候使い、声優さんとは一切関係ありません。
以下の役者さんのコメントから、天候使いの名前と扱う天候と、演じた役者さんの対応を当ててください。自分のことを他人のように言っている人はいません。(このコメントはパズルのための架空のものです)
みついし「ソルト役の人は太陽使いの演技に苦労していましたね。わたしは雪使い役ではありませんでした」
（コメントをいただきました。修正します）→みついし「ソルトは太陽使いでしたが、ソルト役の役者さんは演技に苦労していましたね。わたしは雪使い役ではありませんでした」
みずはし「わたしは風使い役でしたが、シュガーは演じていませんよ。ジンジャーは雨使いですね」
のじま「わたしはターメリック役です。雪使い役の人は、さえきさんに演技の相談をしていたみたいですよ」
今回の記事では、この例題についての記述に終始します。また、Sugarスクリプトに関して、田村先生のページで示されているサンプルから踏み出すことはおそらくありませんので、ご留意ください。
さて。
ヒントから判る情報をマトリックスに記入してみます。以下のようになるのではないでしょうか。
「自分のことを他人のように言っている人はいません」の注意から、みついしさんとソルトの交点、みついしさんと太陽使いの交点、のじまさんと雪使いの交点に×が付くことになります。
この場合、私は、みずはしさんとジンジャーの交点、みずはしさんと風使いの交点には×が付かないという認識でいます。このあたりの認識は揺れるところがある部分かもしれません。
安全に振るなら、
みずはし「わたしは風使い役でしたが、シュガーは演じていませんよ」
あさの「ジンジャーは雨使いですね」
とするのでしょうか。あさのってダレダヨー！ヽ(`Д´)ノ（実在の声優さんとは云々）
でまあ、解くと以下のようになります。
自動解答をもくろむなら、マトリックスとヒント文を入力すれば答えが出力される状況を目指すべきとは思うのですが、ここは志低く、ヒント文を以下のように書き換えます。役者さんとキャラクターを同一視する表現になっていますが、パズル的には問題ないということでよろしく。
・みついしさんはソルトではない ・みついしさんは太陽使いではない ・ソルトは太陽使い ・みついしさんは雪使いではない ・みずはしさんは風使い ・みずはしさんはシュガーではない ・ジンジャーは雨使い ・のじまさんはターメリック ・のじまさんは雪使いではない ・さえきさんは雪使いではない
ここまで準備すれば、sugarの文法に落とすのは簡単ですね。
例えばですが、以下のようになります。
(int sugar 1 1) (int salt 2 2) (int pepper 3 3) (int ginger 4 4) (int turmeric 5 5) (int sun 1 5) (int wind 1 5) (int cloud 1 5) (int rain 1 5) (int snow 1 5) (alldifferent sun wind cloud rain snow) (int kawa 1 5) (int sae 1 5) (int noji 1 5) (int mizu 1 5) (int mitsu 1 5) (alldifferent kawa sae noji mizu mitsu) (ne mitsu salt) (ne mitsu sun) (eq salt sun) (ne mitsu snow) (eq mizu wind) (ne mizu sugar) (eq ginger rain) (eq noji turmeric) (ne noji snow) (ne sae snow)
sugarでコメントが書けるといいのになーと思わなくもないです。
(追記。書けます。;←以降がコメント)
項目を1,2,3,4,5の数字に対応させておき、その関係性をその下で記述しています。名前の項目と数字の対応をこの時点で確定させておく必要は解くという意味ではないですが、後で唯一解性を確認するために確定させています。
結果はこちら。
s SATISFIABLE a sugar 1 a salt 2 a pepper 3 a ginger 4 a turmeric 5 a sun 2 a wind 3 a cloud 5 a rain 4 a snow 1 a kawa 1 a sae 2 a noji 5 a mizu 3 a mitsu 4 a
1に対応する項目を拾っていくと、sugar-snow-kawaとなっています。
他の数字についての対応も確認できるものと思います。
唯一解を確認するためには、この解答を否定する条件をスクリプトに追加します。追加する文は以下のような感じ。
(or (ne sugar 1) (ne salt 2) (ne pepper 3) (ne ginger 4) (ne turmeric 5) (ne sun 2) (ne wind 3) (ne cloud 5) (ne rain 4) (ne snow 1) (ne kawa 1) (ne sae 2) (ne noji 5) (ne mizu 3) (ne mitsu 4) )
これをスクリプトに追加して走らせると、そんなもん答えがネーヨ！ヽ(`Д´)ノと、浅、いやSugarくんが返答してくれます。めでたしめでたし。
ということで今回はここまで。
