Sugarを急遽使用することになったので、
MiniSatとSugarを新たに購入したMacに導入してみました。
-
MiniSat: 充足可能問題の解を導出するSATソルバーの1つ。
(参考：MiniSat公式HP) -
Sugar: SAT型の制約ソルバー。高速なMiniSatを用いる。
(参考：Sugar公式HP)
今回の環境 (前提)
- macOS Sierra 10.12.1
- Homebrew "1.1.1"
- gcc version 5.4.0
- Java 5導入済み
- Perl 5導入済み (Macのデフォルト)
MiniSat導入
公式HPからダウンロードして、パッチ適用やutils/System.ccを書き換えなどが必要…と思いきや、Homebrewで簡単にインストールできることが判明！ 以下のコマンドから、インストールできます。
1. インストール
$ brew install minisat
<実行結果>
==> Downloading https://homebrew.bintray.com/bottles/minisat-2.2.0.el_capitan.bo
######################################################################## 100.0%
==> Pouring minisat-2.2.0.el_capitan.bottle.1.tar.gz
🍺 /usr/local/Cellar/minisat/2.2.0: 4 files, 91.8K
2. 実行確認
以下のコマンドで、適当なディレクトリにてMiniSatが実行できるか確かめてみます。
$ minisat
以下のようなものが出れば成功です。
<実行結果>
Reading from standard input... Use '--help' for help.
============================[ Problem Statistics ]=============================
| |
Sugar導入
1. インストール
Sugar公式HPから最新版Version 2.2.1(sugar-v2-2-1.zip)をダウンロードして解凍。
ダウンロードしたフォルダに移動します。
$ cd sugar-v2-2-1/bin
環境設定する必要があるため、このbin内のsugarを以下のように自分の環境に合わせて編集する。
my $version = "v2-2-1";
my $java = "java";
my $jar = "/Users/ユーザ名/Desktop/sugar-v2-2-1/bin/sugar-v2-2-1.jar"; //ダウンロードしたファイル内のjarファイルの位置を指定
my $solver0 = "/usr/local/bin/minisat";
my $solver0_inc = "minisat-inc";
my $tmp = "/Users/ユーザ名/Desktop/sugar-v2-2-1/tmp_sugar/sugar$$"; //tmp_sugarなどの適当なディレクトリをあらかじめ作成しておき、指定
その後、usr/local/binにsugarを移します。
$ mv sugar /usr/local/bin
これでひとまず導入は完了です。
2. 実行確認
次に、minisatと同じく、適当なディレクトリにてSugarが実行できるか確かめてみます。
$ sugar
出力として、help的なものが出れば成功です。
Sugar実行例
$ sugar [options] cspfile名で実際にcspファイルを実行できます。
試しに、 ダウンロード場所/sugar-v2-2-1/examplesに移り、exampleの1つを実行してみます。
$ sugar nqueens-8.csp
<実行結果>
s SATISFIABLE
a q_1 7
a q_2 2
a q_3 4
a q_4 1
a q_5 8
a q_6 5
a q_7 3
a q_8 6
a
上記のような1つの解が出れば、成功です。