Sugarを急遽使用することになったので、
MiniSatSugarを新たに購入した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つの解が出れば、成功です。

Sign up for free and join this conversation.
Sign Up
If you already have a Qiita account log in.