※現在、ブログ記事を移行中のため一部表示が崩れる場合がございます。
順次修正対応にあたっておりますので何卒ご了承いただけますよう、お願い致します。

SEND+MORE=MONEYを解くsugarのプログラム


2017年 12月 27日

覆面算 SEND + MORE = MONEY を解くsugarプログラムを、いきなりだが見てみよう。

sendmoremoney.csp
; S E N D + M O R E = M O N E Y
(domain range 0 9)
(int S range)
(int E range)
(int N range)
(int D range)
(int M range)
(int O range)
(int R range)
(int Y range)
(!= S 0)
(!= M 0)
(alldifferent S E N D M O R Y)
(=
(+ (+ (* (+ (* (+ (* S 10) E) 10) N) 10) D)
(+ (* (+ (* (+ (* M 10) O) 10) R) 10) E))
(+ (* (+ (* (+ (* (+ (* M 10) O) 10) N) 10) E) 10) Y))
これだけで、覆面算をやってくれる。 これだけ見ると括弧だらけで、まるでLispみたいだと思うだろう。
とりあえず走らせてみて、どうなるか考えよう。
sugarの次に、sugarファイルを書くだけだ。
$ sugar sendmoremoney.csp
s SATISFIABLE
a S	9
a E	5
a N	6
a D	7
a M	1
a O	0
a R	8
a Y	2
a
SATISFIABLEと出ているので、解が存在したことを知らせており、その後ろに書く変数の名前と値がペアになって表示されている。
もし解が存在しないと、UNSATISFIABLEと表示され、変数の値は示されない。
なお、解があったからといって、唯一解である保証はない。

この簡単なプログラムは説明不要と思うが、以下に説明を試みる。

(domain range 0 9)
0から9の間の整数値に対して、rangeという名前をつける。

(int S range)
整数型で定義域がrangeである変数Sを宣言する。
以下のENDMORYを含めて使用されている全8文字(変数)の定義域も同じに宣言する。

(!= S 0)
Sは0でない。 Mも0でない。

(alldifferent S E N D M O R Y)
宣言した変数が互いに異なることを宣言している。 sugarでは、alldifferent はとても良く使われる。

(=
(+ (+ (* (+ (* (+ (* S 10) E) 10) N) 10) D)
(+ (* (+ (* (+ (* M 10) O) 10) R) 10) E))
(+ (* (+ (* (+ (* (+ (* M 10) O) 10) N) 10) E) 10) Y))
これは、とてもごちゃごちゃしているように見えるが、算術計算で普通の記述ができないので長くなっているだけで、下と同じ意味になる。
(((S*10) + E)*10 + N)*10 + D    +    (((M*10) + O)*10 + R)*10 + E
==  ((((M*10) + O)*10 + N)*10 + E)*10 + Y
以上で、SEND + MORE = MONEY を定義した。
さて、どのように調べるか、そのアルゴリズムは、書かなくてよい。
つまり制約条件をここまで書いてきたのだが、それだけでよく、そもそもこのsugarというプログラミング言語は、そもそもアルゴリズムを受け付けないのだ。

sugarとは、こんな感じのプログラミング言語である。
詳しいことは、sugarのホームページを参照のこと。
文法:Syntax of Sugar CSP description

こんな96ページもあるプレゼン資料も存在する。
Solving Constraint Satisfaction Problems with SAT Technology

sugarには制御文はなく、どのように調べてくれているのか分からない。
まあ、そんなこと分からなくても、結果が全ての条件を満たしていればOKである。

sugarでプログラムを書く時、プログラムの動きは考えない。
与えられた問題を、どのようにsugarの文法を使って制約条件を書くか、それは脳トレになる。
発想から変えないとプログラムができない。

覆面算は、SATで扱いやすいタイプの問題である。
実際には、もっともっと制約条件ががんじがらめになっているスケジュール問題などに使うことが多い。