TIM Labs

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

| コメント(0) | トラックバック(0)
覆面算 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で扱いやすいタイプの問題である。
実際には、もっともっと制約条件ががんじがらめになっているスケジュール問題などに使うことが多い。

トラックバック(0)

トラックバックURL: http://labs.timedia.co.jp/mt/mt-tb.cgi/703

コメントする

このブログ記事について

このページは、fujiが2017年12月27日 00:00に書いたブログ記事です。

ひとつ前のブログ記事は「制約充足問題を解くためにsugarをインストール」です。

次のブログ記事は「謹賀新年 平成30年元旦 ナンプレ2題」です。

最近のコンテンツはインデックスページで見られます。過去に書かれたものはアーカイブのページで見られます。