開発環境

Table of Contents

1 build-essentail, C++

  1. 基本開発環境のbuild-essentailをインストールする.
    $ sudo apt-get -y install build-essential
    
  2. g++をインストールする.
    $ sudo apt-get -y install g++
    
  3. zlibをインストールする.
    $ sudo apt-get -y install zlib1g-dev
    
  4. 64 bit環境なら以下をインストールする.
    $ sudo apt-get install libc6-dev-i386
    

2 Java JDK

  1. Java JDK (OpenJDK 6)をインストールする.
    $ sudo apt-get -y install default-jdk
    

    バージョンは以下のようにして確認できる.

    $ java -version
    java version "1.6.0_23"
    OpenJDK Runtime Environment (IcedTea6 1.11pre) (6b23~pre11-0ubuntu1.11.10.2)
    OpenJDK Server VM (build 20.0-b11, mixed mode)
    $ javac -version
    javac 1.6.0_23
    
  2. Eclipseをインストールする.
    $ sudo apt-get -y install eclipse
    
  3. Eclipseの日本語化パッケージをインストールする.
    $ sudo apt-get -y install pleiades
    $ cp /etc/eclipse.ini /tmp
    $ echo "-javaagent:/usr/lib/eclipse/plugins/jp.sourceforge.mergedoc.pleiades/pleiades.jar" >>/tmp/eclipse.ini
    $ sudo mv /etc/eclipse.ini /etc/eclipse.ini.old
    $ sudo mv /tmp/eclipse.ini /etc
    $ eclipse -clean
    

2.1 Ubuntu 12.04 にアップグレードして動かなくなった場合

以下のようにする.

$ cd ~
$ mv .eclipse .eclipse.old

3 SATソルバー

3.1 MiniSat

MiniSatは最も有名なSATソルバーの一つ.

  1. http://minisat.se からソースパッケージをダウンロードし,展開する.
    $ cd /usr/local/src
    $ wget http://minisat.se/downloads/minisat-2.2.0.tar.gz
    $ tar xvzf minisat-2.2.0.tar.gz
    
  2. コンパイルする.
    $ cd minisat
    $ export MROOT=`pwd`
    $ cd core; make rs; cd ..
    $ cd simp; make rs; cd ..
    
  3. /usr/local/bin ディレクトリにインストールする.
    $ cp -p core/minisat_static /usr/local/bin/minisat22_core
    $ cp -p simp/minisat_static /usr/local/bin/minisat22_simp
    
  4. minisatminisat22_core が起動するようにシンボリックリンクを作成する.
    $ cd /usr/local/bin
    $ ln -s minisat22_core minisat
    

3.2 Glucose

GlucoseはSAT 2011 competitionの Application/SAT+UNSAT で優勝. SAT 2009 competitionの Application/UNSAT で優勝.

  1. http://www.lri.fr/~simon/?page=glucose からソースパッケージをダウンロードし,展開する.
    $ cd /usr/local/src
    $ wget http://www.lri.fr/~simon/downloads/glucose-2-compet.tgz
    $ tar xvzf glucose-2-compet.tgz
    
  2. 64bitでビルドする場合には,以下を行なっておく.
    $ cd glucose_2.0/sources/SatELite/ForMani
    $ rm ADTs/*.or Global/*.or
    $ mv template.mak template.mak.orig
    $ sed -e 's/-m32 //' template.mak.orig >template.mak
    $ cd /usr/local/src
    
  3. コンパイルする.
    $ cd glucose_2.0
    $ chmod +x build.sh
    $ ./build.sh
    
  4. /usr/local/bin ディレクトリにインストールする.
    $ cp -p glucose_static /usr/local/bin/glucose20_core
    $ cp -p SatELite_release /usr/local/bin
    $ cp -p glucose.sh /usr/local/bin/glucose20_simp
    $ chmod +x /usr/local/bin/glucose20_simp
    
  5. /usr/local/bin/glucose20_simp をgedit, nano等のエディタで開いて編集する.
    • 4行目を以下のように修正
        echo "USAGE: $0 <input CNF>"
      
    • 13行目を以下のように修正
      mypath=/usr/local/bin
      
    • 18行目を以下のように修正
      RS=$mypath/glucose20_core
      
  6. glucoseglucose20_core が起動するようにシンボリックリンクを作成する.
    $ cd /usr/local/bin
    $ ln -s glucose20_core glucose
    

3.2.1 TODO 注意

最新は glucose 2.1 ( 2012-10-01 月 時点)

3.3 GlueMiniSat

GlueMiniSatはSAT 2011 competitionの Application/UNSAT で優勝.

  1. https://sites.google.com/a/nabelab.org/glueminisat/ からソースパッケージをダウンロードし,展開する.
    $ cd /usr/local/src
    $ wget http://glueminisat.nabelab.org/home/download/glueminisat-2.2.5.tar.gz
    $ tar xvzf glueminisat-2.2.5.tar.gz
    
  2. コンパイルする.
    $ cd glueminisat-2.2.5
    $ export MROOT=`pwd`
    $ cd core; make r; cd ..
    $ cd simp; make r; cd ..
    
  3. /usr/local/bin ディレクトリにインストールする.
    $ cp -p core/glueminisat_release /usr/local/bin/glueminisat225_core
    $ cp -p simp/glueminisat_release /usr/local/bin/glueminisat225_simp
    
  4. glueminisatglueminisat225_core が起動するようにシンボリックリンクを作成する.
    $ cd /usr/local/bin
    $ ln -s glueminisat225_core glueminisat
    

3.4 Clasp

ClaspはSAT 2011 competitionの Crafted/UNSAT で優勝. SAT 2009 competitionの Crafted/SAT+UNSAT, Crafted/SAT で優勝.

  1. http://www.cs.uni-potsdam.de/clasp/ からパッケージをダウンロードし,展開する.
    • http://sourceforge.net/projects/potassco/files/clasp/2.0.6/ を開き clasp-2.0.6-st-x86-linux.tar.gz をクリックし,保存する (64bit なら clasp-2.0.6-st-x86_64-linux.tar.gz).
    • パッケージを展開する.
      $ cd /usr/local/src
      $ mv ~/Downloads/clasp-2.0.6-st-x86-linux.tar.gz .
      $ tar xvzf clasp-2.0.6-st-x86-linux.tar.gz
      
  2. /usr/local/bin ディレクトリにインストールする.
    $ cp -p clasp-2.0.6/clasp-2.0.6-st-x86-linux /usr/local/bin/clasp206
    
  3. claspclasp206 が起動するようにシンボリックリンクを作成する.
    $ cd /usr/local/bin
    $ ln -s clasp206 clasp
    

3.4.1 TODO 注意

最新は clasp 2.1.1 ( 2013-02-01 金 時点)

3.5 PrecoSAT

PrecoSATはSAT 2009 competitionの Application/SAT+UNSAT で優勝.

  1. http://fmv.jku.at/precosat/ からソースパッケージをダウンロードし,展開する.
    $ cd /usr/local/src
    $ wget http://fmv.jku.at/precosat/precosat-576-7e5e66f-120112.tar.gz
    $ tar xvzf precosat-576-7e5e66f-120112.tar.gz
    
  2. コンパイルする.
    $ cd precosat-576-7e5e66f-120112
    $ ./configure
    $ make
    
  3. /usr/local/bin ディレクトリにインストールする.
    $ cp -p precosat /usr/local/bin/precosat576
    
  4. precosatprecosat576 が起動するようにシンボリックリンクを作成する.
    $ cd /usr/local/bin
    $ ln -s precosat576 precosat
    

3.6 Lingeling, Plingeling

LingelingはSAT 2011 competitionの Application/SAT+UNSAT で3位. PlingelingはSAT 2011 competitionの並列ソルバー Application/SAT+UNSAT で優勝.

  1. http://fmv.jku.at/lingeling/ からソースパッケージをダウンロードし,展開する.
    $ cd /usr/local/src
    $ wget http://fmv.jku.at/lingeling/lingeling-587f-4882048-110513.tar.gz
    $ tar xvzf lingeling-587f-4882048-110513.tar.gz
    
  2. コンパイルする.
    $ cd lingeling-587f-4882048-110513
    $ ./configure
    $ make
    
  3. /usr/local/bin ディレクトリにインストールする.
    $ cp -p lingeling /usr/local/bin/lingeling587f
    $ cp -p plingeling /usr/local/bin/plingeling587f
    
  4. シンボリックリンクを作成する.
    $ cd /usr/local/bin
    $ ln -s lingeling587f lingeling
    $ ln -s plingeling587f plingeling
    

3.7 CryptoMiniSat

CryptoMiniSatはSAT Race 2010で優勝.

  1. http://www.msoos.org/cryptominisat2/ からパッケージをダウンロードする.
    $ cd /usr/local/src
    $ mv ~/Downloads/cryptominisat-2.9.4-linux-static32.gz .    2. ~/usr/local/bin~ ディレクトリにインストールする.
    $ gzip -d -c cryptominisat-2.9.4-linux-static32.gz >/usr/local/bin/cryptominisat294
    $ chmod +x /usr/local/bin/cryptominisat294
    
  2. cryptominiastcryptominiast294 が起動するようにシンボリックリンクを作成する.
    $ cd /usr/local/bin
    $ ln -s cryptominiast294 cryptominiast
    

3.8 Sat4j

Sat4j は Java で記述されたSATソルバー. Eclipse にも組み込まれている.

  1. http://www.sat4j.org から sat4j-core-v20111030.zip をダウンロードし,展開する.
    $ cd /usr/local/src
    $ mkdir sat4j-core-v20111030; cd sat4j-core-v20111030
    $ mv ~/Downloads/sat4j-core-v20111030.zip .
    $ unzip sat4j-core-v20111030.zip
    
  2. gedit, nano等のエディタで,以下の内容の /usr/local/bin/sat4j231 を作成.
    #!/bin/sh
    export JAVA_OPTS="-Xmx2000M"
    exec java -jar /usr/local/src/sat4j-core-v20111030/org.sat4j.core.jar $*
    
  3. 実行可能にする.
    $ cd /usr/local/bin
    $ chmod +x sat4j231
    $ ln -s sat4j231 sat4j
    
  4. 起動確認
    $ sat4j
    

3.8.1 TODO 注意

最新は Sat4j 2.3.2 ( 2012-10-01 月 時点)

4 Sugar

SugarはCSP Solver competition 2008, 2009のグローバル制約部門で優勝.

  1. http://bach.istc.kobe-u.ac.jp/sugar/ からソースパッケージをダウンロードし,展開する.
    $ cd /usr/local/src
    $ wget http://bach.istc.kobe-u.ac.jp/sugar/package/sugar-v2-1-0.zip
    $ unzip sugar-v2-1-0.zip
    
  2. インストールする.
    $ cd sugar-v2-1-0/bin
    $ make install
    
  3. 例題を動かす.
    $ cd ../examples
    $ sugar nqueens-8.csp
    $ sugar -v nqueens-8.csp
    $ sugar -vv nqueens-8.csp
    $ sugar -solver glucose nqueens-8.csp
    

5 Timeout

  1. https://github.com/pshved/timeout からプログラムをダウンロードし,インストールする.
    $ cd /usr/local/bin
    $ wget https://github.com/pshved/timeout/raw/master/timeout
    $ mv timeout timeout.pl
    $ chmod +x timeout.pl
    
  2. 実行してみる.
    $ cd /usr/local/src/sugar-v1-15-1/examples
    $ timeout.pl -t 60 sugar nqueens-200.csp >/dev/null
    FINISHED CPU 27.57 MEM 1277360 MAXMEM 1368556 STALE 1
    <time name="ALL">27440</time>
    $ timeout.pl -t 10 sugar nqueens-200.csp >/dev/null
    TIMEOUT CPU 10.14 MEM 1363544 MAXMEM 1373808 STALE 0
    <time name="ALL">10170</time>
    $ timeout.pl -t 60 -p 'sat,SAT;java,JAVA' sugar nqueens-200.csp >/dev/null
    FINISHED CPU 25.32 MEM 1277056 MAXMEM 1369936 STALE 1
    <time name="SAT">8480</time>
    <time name="JAVA">16690</time>
    

6 色々なSATソルバーを比較する

  1. 準備
    $ cd
    $ mkdir sugar
    $ cd sugar
    $ cp -p /usr/local/src/sugar-v1-15-1/examples/nqueens-200.csp .
    $ mkdir log
    
  2. 以下のようにして様々なSATソルバーでSugarを実行する (60秒タイムアウト).
    $ for s in minisat glucose glueminisat clasp precosat lingeling; do
    > echo $s
    > timeout.pl -t 60 sugar -vv -solver $s nqueens-200.csp >log/nqueens-200-$s.log 2>&1
    > done
    
  3. それぞれの結果は log/nqueens-200-minisat.log などに保存されている.
  4. それぞれが何秒で終わったのかを調べる.
    $ grep FINISHED log/nqueens-200-*.log
    log/nqueens-200-glucose.log:FINISHED CPU 29.17 MEM 8456 MAXMEM 1379504 STALE 1
    log/nqueens-200-minisat.log:FINISHED CPU 23.89 MEM 1277120 MAXMEM 1385472 STALE 1
    $ grep TIMEOUT log/nqueens-200-*.log
    log/nqueens-200-clasp.log:TIMEOUT CPU 60.03 MEM 572004 MAXMEM 1383060 STALE 1
    log/nqueens-200-glueminisat.log:TIMEOUT CPU 60.09 MEM 996520 MAXMEM 1370052 STALE 1
    log/nqueens-200-lingeling.log:TIMEOUT CPU 60.08 MEM 1603064 MAXMEM 2007664 STALE 1
    log/nqueens-200-precosat.log:TIMEOUT CPU 60.13 MEM 1723788 MAXMEM 1744864 STALE 1
    

6.1 CSVファイルにまとめる

  1. Perl のプログラム summary.pl をダウンロードする.
    $ mv ~/Downloads/summary.pl .
    $ chmod +x summary.pl
    
  2. 実行して,CSVファイルを作成する.
    $ ls log/* | ./summary.pl >nqueens-200.csv
    
  3. nqueens-200.csv の内容を確認する (「q」をタイプすると less コマンドが終了する).
    $ less nqueens-200.csv
    

    内容は以下の通り.

    #FILE FIN RESULT OPT SAT_COUNT CPU CPU_ENCODE CPU_SOLVE MAXMEM VARS CLAUSES BYTES
    log/nqueens-200-clasp.log TIMEOUT UNKNOWN ? 1 60.03 17.99 ? 1383060 159196 18646098 407057282
    log/nqueens-200-glucose.log FINISHED SATISFIABLE ? 1 29.17 17.11 12 1379504 159196 18646098 407057282
    log/nqueens-200-glueminisat.log TIMEOUT UNKNOWN ? 1 60.09 17.59 ? 1370052 159196 18646098 407057282
    log/nqueens-200-lingeling.log TIMEOUT UNKNOWN ? 1 60.08 20.23 ? 2007664 159196 18646098 407057282
    log/nqueens-200-minisat.log FINISHED SATISFIABLE ? 1 23.89 16.51 7.41 1385472 159196 18646098 407057282
    log/nqueens-200-precosat.log TIMEOUT UNKNOWN ? 1 60.13 18.49 ? 1744864 159196 18646098 407057282
    

    各行は左から順に以下を表す.

    番号欄名内容
    1FILEログファイル名
    2FINTIMEOUT: タイムアウト,FINISHED: 完了
    3RESULTSATISFIABLE: 充足可能,UNSATISFIABLE: 充足不能,OPTIMUM: 最適解,UNKNOWN: 不明
    4OPT最適化問題の場合は最適値.判定問題の場合は "?"
    5SAT_COUNTSATソルバーの起動回数 (判定問題の場合は 1)
    6CPU総CPU時間 (秒)
    7CPU_ENCODE符号化のCPU時間 (秒)
    8CPU_SOLVE符号化を除くCPU時間 (秒) (SATソルバーと復号化のCPU時間の合計)
    9MAXMEM最大メモリ使用量 (1Kバイト=1024バイト単位)
    10VARSSATの変数の数
    11CLAUSESSATの節の数
    12BYTESSATのファイルサイズ (バイト単位)
    • CPU = CPU_ENCODE + CPU_SOLVE がほぼ成り立つはずだが,誤差がある.
  4. LibreOffice Calcで開く.
    $ soffice nqueens-200.csv
    
    • 「スペース」にチェックを付ける.

6.2 色々調べる

  1. FINISHEDの個数を調べる.
    $ grep FINISHED nqueens-200.csv | wc -l
    
    • grep はパターンにマッチした行だけを取り出す.
    • wc -l は行数を数える.
  2. CPU時間の昇順でソートする.
    $ sort -k 6 -n nqueens-200.csv
    
    • -k はキーの欄の番号(左端が1)を指定するオプション
    • -n は数値としてソートするオプション (無しの場合,文字列としてソートされる)
  3. FINISHEDのものをCPUの降順でソートする.
    $ grep FINISHED nqueens-200.csv | sort -k 6 -n -r
    
    • -r は降順を指定するオプション
  4. 最も速かったものだけ表示する.
    $ grep -v '^#' nqueens-200.csv | sort -k 6 -n | head -1
    
    • grep -v はパターンにマッチしない行だけを取り出す.
    • ^ は行の先頭にマッチする正規表現
    • head は先頭から指定した行数だけ取り出す.
  5. FINISHEDで最も遅かったものだけ表示する.
    $ grep FINISHED nqueens-200.csv | sort -k 6 -n -r | head -1
    
  6. FINISHEDについてメモリ順でソートする.
    $ grep FINISHED nqueens-200.csv | sort -k 9 -n
    
  7. average.pl をダウンロードして使用すると,算術平均,幾何平均などを求めることができる.
    $ mv ~/Downloads/average.pl .
    $ chmod +x average.pl
    $ grep FINISHED nqueens-200.csv | ./average.pl -k 6
    count 2 total 42.32 amean 21.16 gmean 21.1206415622253 min 19.87 max 22.45
    
    名前
    countデータ数
    total総和
    amean算術平均
    gmean幾何平均
    min最小値
    max最大値

7 さらに大規模な実験

  1. 準備
    $ cp -p /usr/local/src/sugar-v1-15-1/tools/misc/nqueens.pl .
    $ mkdir log-nqueens
    
  2. テキストファイル solvers.txt をダウンロードする.
    $ mv ~/Downloads/solvers.txt .
    
  3. Perl のプログラム run-nqueens.pl をダウンロードする.
    $ mv ~/Downloads/run-nqueens.pl .
    $ chmod +x run-nqueens.pl
    
  4. プログラムを見てみる (「q」をタイプすると less コマンドが終了する).
    $ less run-nqueens.pl
    
    • このプログラムは n が 10, 20, 30, …, 150 の15通りの n-クイーン問題について, solvers.txt に書かれている9種類のSATソルバーを使用して求解を行う. タイムアウトは60秒である.
    • 結果のログファイルは log-nqueens ディレクトリ中に作成される.
  5. バックグラウンドで実行を開始する(30分程度かかる).
    $ ./run-nqueens.pl >run-nqueens.log &
    
  6. どこまで実行したか見てみる.
    $ tail -f run-nqueens.log
    
    • Ctrl-C で表示を中断する.
  7. 完了したか調べる.
    $ jobs
    
  8. TIMEOUTがあるか調べる.
    $ ls log-nqueens/* | ./summary.pl | grep TIMEOUT
    
  9. 完了したら,csvファイルを作成する.
    $ ls log-nqueens/*.log | ./summary.pl >nqueens-all.csv
    

7.1 色々調べてみよう

  1. precosat576 で解けた問題数や平均CPU時間は以下のようにして調べられる.
    $ grep precosat576 nqueens-all.csv | grep FINISHED | ./average.pl -k 6
    
  2. 全SATソルバーの解けた問題数などを一気に表示して見よう.
    $ for s in `cat solvers.txt`; do
    > echo -n "$s "
    > ...
    > done
    

    上の「…」の部分のコマンドを適切に書くと,以下のように表示される.

    minisat22_core count 15 total 137.22 amean 9.148 gmean 6.32624018300231 min 0.34 max 18.99
    minisat22_simp count 14 total 292.48 amean 20.8914285714286 gmean 10.6987987051456 min 0.33 max 59.84
    glucose20_core count 15 total 179.39 amean 11.9593333333333 gmean 7.63370197264108 min 0.32 max 30.85
    glucose20_simp count 15 total 248.83 amean 16.5886666666667 gmean 9.86548404469626 min 0.28 max 32.81
    glueminisat225_core count 15 total 170.07 amean 11.338 gmean 7.35201352023131 min 0.31 max 30.11
    glueminisat225_simp count 14 total 264.71 amean 18.9078571428571 gmean 9.92440232268175 min 0.32 max 52.73
    clasp205 count 14 total 213.99 amean 15.285 gmean 9.07680926861466 min 0.33 max 45.13
    precosat576 count 10 total 132.85 amean 13.285 gmean 6.08354390034021 min 0.26 max 53.59
    lingeling587f count 14 total 356.27 amean 25.4478571428571 gmean 14.0073371782796 min 0.40 max 54.72
    
  3. 上のプログラムを nqueens-all-result.sh として保存し,実行可能にしよう.
    $ chmod +x nqueens-all-result.sh
    
  4. 以下のように記述すると解けた問題数 (第3欄)の多いものから順に表示される.
    $ ./nqueens-all-result.sh | sort -k 3 -n -r
    
  5. さらに全15問が解けたものについて,平均CPU時間 (第5欄)の昇順にソートしてみよう.
    $ ./nqueens-all-result.sh | grep " count 15 " | sort -k 5 -n
    

8 gnuplot

  1. インストールする.
    $ sudo apt-get -y install gnuplot
    
  2. gnuplot のプログラム nqueens-all-cactus.plot をダウンロードする.
    $ mv ~/Downloads/nqueens-all-cactus.plot .
    
  3. gnuplot のプログラムを実行し,EPSファイルを作成する.
    $ gnuplot nqueens-all-cactus.plot
    
  4. EPSファイルをPNGファイルに変換する.
    $ convert -density 300 nqueens-all-cactus.eps nqueens-all-cactus.png
    
    • このようなグラフをcactus plotという.

nqueens-all-cactus.png

9 Copris

  1. scalaをインストールする.
    $ sudo apt-get -y install scala
    
  2. http://bach.istc.kobe-u.ac.jp/copris/ からソースパッケージをダウンロードし,展開する.
    $ cd /usr/local/src
    $ wget http://bach.istc.kobe-u.ac.jp/copris/copris-v2-0-0.zip
    $ unzip copris-v2-0-0.zip
    
  3. 例題を動かす.
    $ cd copris-v2-0-0/examples
    $ scalac -cp ../lib/copris-all-v2-0-0.jar -d classes Examples.scala
    $ scala -cp classes:../lib/copris-all-v2-0-0.jar FirstStep
    $ scala -cp classes:../lib/copris-all-v2-0-0.jar Queens 8
    $ scala -cp classes:../lib/copris-all-v2-0-0.jar PerfectSquare
    

10 TODO PBSugar

  1. http://bach.istc.kobe-u.ac.jp/pbsugar/ からソースパッケージをダウンロードし,展開する.
    $ cd /usr/local/src
    $ wget http://bach.istc.kobe-u.ac.jp/pbsugar/pbsugar-v1-0-3.zip
    $ unzip pbsugar-v1-0-3.zip
    
  2. インストールする.
    $ cd pbsugar-v1-0-3/bin
    $ make install
    
  3. 例題を動かす.
    • PB Competitions の例題が必要

11 リンク

Date: 2013-10-08 14:50:10 JST

Author: 田村直之

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0