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

覆面算　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と表示され、変数の値は示されない。
なお、解があったからといって、唯一解である保証はない。

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

(=
(+ (+ (* (+ (* (+ (* 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で扱いやすいタイプの問題である。
実際には、もっともっと制約条件ががんじがらめになっているスケジュール問題などに使うことが多い。