TIM Labs

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

| コメント(0) | トラックバック(0)
制約充足問題(Constraint satisfaction problem, CSP)というのをご存知だろうか?
まったく文字通りの意味で、たくさんの制約が与えられて、それらの制約を全部充たす(充足する)解を求める問題だ。
まず、Wikipediaへのリンク(制約充足問題)を示しておく。

制約は、要請、必須条件とか、ルールという言葉に置き換えても良い。
言葉で説明しているだけだと難しいが、実例があればわかりやすいので、1つ例をあげる。

   S E N D
 + M O R E
------------------
  M O N E Y

文字には0〜9の数字を入れます。
同じ文字には同じ数字、異なる文字には異なる数字を入れます。
また、最上位桁の文字には、0は入りません。
例は覆面算であり、色々な制約(といっても小学生でも説明不要なような制約なんだが)があって、それらを全て満足するように文字に数字を当てはめる。

各英大文字には、0〜9の数字が入る。
同じ英大文字は同じ数字になり、異なる英大文字は異なる数字となる。
最上位桁の数字は0にはならない。
さて、これをどうやって解こうか。
条件をいちいち調べれば解けるはずだが、そんな面倒なことをプログラマがやるようではまずい。プログラマたるもの、横着でなければいけない。 と
いうことで、条件だけ書けば解いてくれる便利なプログラムはないものかと以前探した時に見つけてつかったことがあるのが、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
これは8クィーンで、8x8のチェス盤上に、どのクィーンも他のクィーンに取られない(利き筋にない)ように置く配置を求める問題である。 答えは、各列の何マス目に置けば良いかを示している。
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のプログラムは次回に説明しよう。

トラックバック(0)

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

コメントする

このブログ記事について

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

ひとつ前のブログ記事は「書評:『Chainerで学ぶディープラーニング入門』」です。

次のブログ記事は「SEND+MORE=MONEYを解くsugarのプログラム」です。

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