Sugarと制約ソルバーcryptominisatの開発環境の構築

この記事では、Sugarと制約ソルバーcryptominisatを利用した開発環境の構築の流れを紹介します。

はじめに

開発環境構築の記事を書こうと思ったきっかけは、Sugar導入に関する記事が少なすぎたからです。

また、一般的にはSugarと言ったら、Minisatを利用する様ですが、私の環境ではMinisatがうまく起動しなかったのでcryptominisatを導入しています。

本当にたくさんのたくさんの時間をこのツール導入に割いてしまったので、皆さんのためになればと思います。

開発環境

環境は以下になります。

• macOS Mojave 10.14.5
• Homebrew 2.1.6

私はmacでツールを導入するので、Windowsの方などには参考にならない内容があるかもしれません。

まず、Homebrewをインストールする必要性があるので、まだインストールしていないという方はこちらのリンクからインストールをしてください。

Homebrewのインストールページへ

brewがインストールできたらターミナルで以下のコマンドを打って、インストールが完了しているのか確認しましょう。

$ brew doctor

リターン(エンター)を押します。

Your system is ready to brew.

この表示が出力されたらインストール完了です。

次はSugarのインストールをしていきます。

Sugarのインストール

Sugarをインストールします。

下記のリンクからSugar公式ホームページにとんでください。

Sugar公式HPへ

ホームページを下にスクロールしていくとDownloadの項目があります。

今現在リリースされている最新版sugar-v2.3.3なので、これをクリックして、ダウンロードします。

ダウンロードが終了したら、このフォルダを好きな場所(デスクトップなど)に移動してください。

この後sugarにパスを通します。

Sugarにパスを通す

Unixコマンドで、lsやcd、pwdなどはディレクトリの階層に関係なくコマンドを実行することができます。

どのディレクトリにいてもコマンドを実行できる理由は、実行ファイルにパスが通っているからです。

sugarでも、パスを通す必要があるので、パスの通し方を簡単に説明していきます。

ターミナルで以下を実行してください。

$ vi ~/.bash_profile

これを実行すると画面が切り替わり、上の方にexport PATH=~~~~みたいな感じで表示されていると思います。

これが現在自分が通しているパスのリストになります。

iを押すとInsertモードに切り替わるのでiを押してください。

これはパスを入力する時のイメージです。

export PATH=$PATH:自分が通したいPATH

自分が通したいPATHに/sugar/binまでのパスを挿入してください。

完了したらescキーを押して、Insertモードを抜けます。

:wqと入力してreturnキーを押して保存しましょう。

これでパスを通す作業は完了です。

sugarにパスが通ったか確認してみましょう！

このコマンドを実行してください。

$ sugar

こんな感じで出力されたら、パスが通ってます。

制約ソルバーcryptominisatのインストール

ターミナルを起動します。

ターミナルで以下を実行してください。

$ brew install cryptominisat

これを実行すると、cryptominisatのインストールが始まります。

cryptominisatのインストールはこれで完了です。

Sugarの環境設定

最後に、Sugarの環境設定をする必要があります。

sugar/bin内にある、sugarをエディタで開いてください。

sugar内のこの部分を修正する必要があります。

my $version = "v2-2-3";
my $java = "java";
my $jar = "sugarまでのパス/sugar-v2-2-1/bin/sugar-v2-2-3.jar";  //jarファイルの位置を指定
my $solver0 = "cryptominisatのUnix実行ファイルまでのパス";
my $solver0_inc = "minisat-inc";
my $tmp = "/Users/ユーザ名/Desktop/sugar-v2-2-1/tmp_sugar/sugar$$";  //tmp_sugarは自分で作成したもの

この環境設定が完了すれば環境構築は終了です！

では、実際にcspファイルを実行してみましょう。

sugarのexamplesフォルダ内のファイルが例題です。

今回nqueens-8.cspを実行してみます。

ディレクトリをexamplesに移ってください。

移ったら以下のコマンドを実行してください。

$ 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

以上で終了です！お疲れ様でした！！

おわりに

いかがでしたでしょうか。

Sugarとcryptominisatの導入手順を筆者なりにわかりやすく紹介しました。

この記事を読むことで、みなさんがツール導入に無駄な時間が取られないことを願っております！