制約充足問題を解くためにsugarをインストール

例は覆面算であり、色々な制約（といっても小学生でも説明不要なような制約なんだが）があって、それらを全て満足するように文字に数字を当てはめる。

各英大文字には、０〜９の数字が入る。
同じ英大文字は同じ数字になり、異なる英大文字は異なる数字となる。
最上位桁の数字は０にはならない。

さて、これをどうやって解こうか。
条件をいちいち調べれば解けるはずだが、そんな面倒なことをプログラマがやるようではまずい。プログラマたるもの、横着でなければいけない。 と
いうことで、条件だけ書けば解いてくれる便利なプログラムはないものかと以前探した時に見つけてつかったことがあるのが、sugarというものだ。
昔使っていたのだが、最近また制約充足問題関連の話があって、使おうとしたら、パソコンから消滅していた。
 ということで、まずはインストールだ。

 神戸大学の田村先生が用意してくれている Sugar: a SAT-based Constraint Solverに説明があるので、この通にやればインストールできる。
実際にインストールしてみるには、SATソルバーMiniSatとSugarを導入の方が分かりやすい。
日本語だし。

sugarの実行ファイルはperlになっていて、その先頭部分をインストールした環境に合わせるようになっている。
インストールしたものは、以下のように変更した。
SATソルバーは色々世の中というか、世界には転がっているのだが、前回も使ったminisatを使うことにしたので、もちろんこれもインストールしておかないといけない。
 

my $version = "v2-3-2";
my $java = "java";
my $jar = "/usr/local/lib/sugar/sugar-$version.jar";
## my $solver0 = "glucose";
my $solver0 = "/usr/local/bin/minisat";
my $solver0_inc = "minisat-inc";
my $tmp = "/tmp/sugar$$";

インストールが済んだら、とりあえず動かしてみよう。
sugarをインストールしたとき、/example/ の下にsugarのサンプルコードが入っている。
拡張子は .csp である。

examples$ sugar nqueens-8.csp
s SATISFIABLE
a q_1	4
a q_2	2
a q_3	8
a q_4	6
a q_5	1
a q_6	3
a q_7	5
a q_8	7
a

これは８クィーンで、８ｘ８のチェス盤上に、どのクィーンも他のクィーンに取られない（利き筋にない）ように置く配置を求める問題である。 答えは、各列の何マス目に置けば良いかを示している。
sugarのプログラムnqueens-8.cspは以下であるが、説明は略す。

; 8-Queens Problem
(int q_1 1 8)
(int q_2 1 8)
(int q_3 1 8)
(int q_4 1 8)
(int q_5 1 8)
(int q_6 1 8)
(int q_7 1 8)
(int q_8 1 8)
(alldifferent q_1 q_2 q_3 q_4 q_5 q_6 q_7 q_8)
(alldifferent (+ q_1 1) (+ q_2 2) (+ q_3 3) (+ q_4 4) (+ q_5 5) (+ q_6 6) (+ q_7 7) (+ q_8 8))
(alldifferent (- q_1 1) (- q_2 2) (- q_3 3) (- q_4 4) (- q_5 5) (- q_6 6) (- q_7 7) (- q_8 8))
; END

あ、長くなったので、SEND+MORE＝MONEYを解くsugarのプログラムは次回に説明しよう。