Sugar制約ソルバーがパズル神

僕はこの方面に完全に素人なのですが,制約充足問題と呼ばれる種類の数学の問題があります.

制約充足問題とは複数の制約条件を満たす状態を見つける,とまあ,ざっくばらんな説明がWikipediaにも載っており,意味不明です.誰か加筆求む.

一方で具体例は,豊かそのもの.数独や充足可能性問題などがこのタイプの問題だそうです.

で,こうしたパズルをコンピュータに解かせるにはどうするか.

手続き型言語でfor文ぶん回して… でもいいが,

「制約条件を与えて,それを命題論理として解く」という何やらエレガントな手法をとって答えを高速に導くのが,紹介するSugarです.

制約充足問題(CSP)を充足可能性問題(SAT)に書き換え(Sugar),それをSATソルバー(Minisat)が解くという流れのようです.

パズルをSugar制約ソルバーで解く によると,ニコリのパズルは尽く解けるようです.

ソースコードも(面倒だが)非常に読みやすく,例えば,数独で「一列全ての数字は異なる」を制約条件で与えたかったら

(allDifferent x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_0_5 x_0_6 x_0_7 x_0_8)

という風に書くだけです!! 素敵!!

 

いつインストールするの!? 今でしょ!!

SugarをMacにインストールする手順をこのエントリーでは紹介します.

SugarはJavaとPerlとMinisatが必要ですが,最初の2つはMacなら最初から入っています.

Minisatをインストールします.

1. Xcodeをインストールします.(すでに持っている場合は不要です)

2. Minisat からダウンロードします.いっぱいありますが,minisat2-070721.zip これでいいと思います.

3. ダウンロードして解凍すると utils/System.cc がありますが,この一番下の方を次のように書き換えます.

#elif defined(__APPLE__)
#include 

double Minisat::memUsed(void) {
   malloc_statistics_t t;
   malloc_zone_statistics(NULL, &t);
   return (double)t.max_size_in_use / (1024*1024); }
double Minisat::memUsedPeak(void) {return memUsed(); }
#else

4. あとは README にあるとおりしますが,”gmake rs”は”make r”に変えます.

export MROOT= (or setenv in cshell)
cd { core | simp }
make r
cp minisat_static /minisat

僕は,

/usr/local/share/minisat/

にインストールしました.

 

最後に,Sugarをインストールします.

1. Sugar: a SAT-based Constraint Solver から package/sugar-v2-0-0.zip をダウンロードします.

2. 解凍して,bin/sugar をテキストエディタで開いて,

- $java : Java command path
 - $jar : Full path of the sugar-v2-0-0.jar file in the same directory
 - $solver : Path of the SAT solver (e.g. MiniSat)
 - $tmp : Path prefix for temporally created files

に従います.(README そのまま)

僕は,

/usr/local/share/sugar

にインストールしました.だから,僕の設定は

my $java = "java";
my $jar = "/usr/local/share/sugar/bin/sugar-$version.jar";
my $solver0 = "/usr/local/share/minisat/core/minisat";
my $solver0_inc = "minisat-inc";
my $tmp = "/usr/local/share/sugar/tmp/sugar$$";

です.

あとは,sugar にシェルからパス通したら幸せになれると思います.

examplesに .csp ファイルのサンプルがあるので,遊んでみてください.

参考 (訳しただけ)

広告

コメントを残す

以下に詳細を記入するか、アイコンをクリックしてログインしてください。

WordPress.com ロゴ

WordPress.com アカウントを使ってコメントしています。 ログアウト / 変更 )

Twitter 画像

Twitter アカウントを使ってコメントしています。 ログアウト / 変更 )

Facebook の写真

Facebook アカウントを使ってコメントしています。 ログアウト / 変更 )

Google+ フォト

Google+ アカウントを使ってコメントしています。 ログアウト / 変更 )

%s と連携中