Knuth版SATソルバーのインストール

Table of Contents

1 概要

本稿では Donald Knuth 先生の名著 The Art of Computer Programming (TAOCP)の 第4巻 Combinatorial Algorithms 中の 7.2.2.2 節 Satisfiability に関し, Knuthが作成し公開しているプログラムのインストール方法について説明する.

また,その他のプログラムについても紹介する.

1.1 注意

本Webページ(およびPDF)の作成には Emacs org-mode を用いており, 数式等の表示は MathJax を用いています. IEでは正しく表示されないことがあるため, Firefox, Safari等のWebブラウザでJavaScriptを有効にしてお使いください. また org-info.js を利用しており, 「m」キーをタイプするとinfoモードでの表示になります. 利用できるショートカットは「?」で表示されます.

2 Knuth版プログラムのインストール

2.1 すべて自分でインストールする

以下はMac OS XあるいはLinuxの環境を前提としている(申し訳ない…). WindowsではMinGW-w64, Cygwin, Linux on Windowsなどを利用する必要があるだろう.

Knuth作のSATソルバーや関連するプログラムは,以下に置かれている.

以下がそれらのプログラムの一覧である(説明はKnuthによる).

  • DIMACS-TO-SAT and SAT-TO-DIMACS : Filters to convert between DIMACS format for SAT problems and the symbolic semantically meaningful format used in the programs below
  • SAT0 : My implementation of Algorithm 7.2.2.2A (very basic SAT solver)
  • SAT0W : My implementation of Algorithm 7.2.2.2B (teeny tiny SAT solver)
  • SAT8 : My implementation of Algorithm 7.2.2.2W (WalkSAT)
  • SAT9 : My implementation of Algorithm 7.2.2.2S (survey propagation SAT solver)
  • SAT10 : My implementation of Algorithm 7.2.2.2D (Davis-Putnam SAT solver)
  • SAT11 : My implementation of Algorithm 7.2.2.2L (lookahead 3SAT solver)
  • SAT11K : Change file to adapt SAT11 to clauses of arbitrary length
  • SAT12 and the companion program SAT12-ERP : My implementation of a simple preprocessor for SAT
  • SAT13 : My implementation of Algorithm 7.2.2.2C (conflict-driven clause learning SAT solver)
  • SAT-LIFE : Various programs to formulate Game of Life problems as SAT problems (July 2013)
  • SAT-NFA : Produce a forcing encoding of regular languages into SAT via nondeterministic finite automata (April 2016)
  • SATexamples : Programs for various examples of SAT in Section 7.2.2.2 of TAOCP; also more than a hundred benchmarks (updated 08 July 2015)

コンパイルには 文芸的プログラミング のシステム CWEB が必要である. それにはTeX Liveのパッケージ (かなり大きい)をインストールするのが恐らく最も簡単だ.

CWEBがインストールされている場合, Knuthのプログラムのダウンロードおよびすべてのインストール作業を行うPerlスクリプトは以下の通り.

ただし,TeX Live (CWEB)に加えperl, curl, tar, gccが必要となる

例えば,以下のように実行すれば良い (30分程度かかる).

$ cd ~/Desktop
$ mkdir -p taocp-sat/knuth
$ cd taocp-sat/knuth
$ curl -O http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/knuth/install.pl
$ perl install.pl | tee install.log

1行目でDesktopに移動している. 2行目でDesktop中に taocp-sat/knuth のフォルダを作成し,3行目でそのフォルダに移動する. 4行目で install.pl を取得し,5行目で実行している.

このスクリプトを実行すると, taocp-sat/knuth 内に以下のディレクトリが作成される.

  • downloads : ダウンロード場所
  • bin : コンパイル後の実行ファイル
  • pdf : PDFファイル
  • sat-examples : SAT examplesのソース,問題ファイル
  • sat-life : SAT lifeのソース
  • sat-solvers : SATソルバーのソース
  • sgb : SGB (Stanford GraphBase)のソース

以下は install.pl の実行ログの例である ("# "で始まる行のコマンドが実行されている).

Knuthが利用しているシステムと同一でないせいか,一部エラーがあるようだ. 利用においては,注意する必要がある.

インストールが成功すれば,以下のようにPATH環境変数を設定する.

$ echo 'export PATH=~/Desktop/taocp-sat/knuth/bin:$PATH' >>~/.profile
$ . ~/.profile

実行してみる.

$ sat13 <sat-examples/benchmarks-SAT/waerden-5-5-177.sat 
(177 variables, 7656 clauses, 38280 literals successfully read)
!SAT!
 67 77 72 76 ~64 69 155 83 ~3 ~84 73 66 ~81 ~75 ~65 78 ~55 71 ~70 60 ~63 ~54 74 ~80 85 ~61 62 53 ~57 ~82 ~90 ~46 59 86 ~88 68 ~93 ~91 ~50 ~95 87 35 110 ~51 ~96 ~47 ~44 ~10 ~135 ~98 92 28 30 115 ~101 ~99 120 25 97 117 102 27 ~107 ~132 ~94 29 32 104 103 79 157 58 ~26 ~31 ~52 ~128 ~137 ~40 ~105 ~49 18 48 39 43 112 118 33 ~11 ~38 ~36 ~126 ~13 42 130 15 41 147 106 22 113 ~17 ~142 ~8 ~125 ~21 ~20 ~37 ~7 ~124 ~114 ~108 ~134 ~109 ~140 ~5 24 14 9 165 116 159 127 16 160 123 121 162 175 131 136 ~6 ~170 ~19 ~145 ~119 ~139 ~138 ~151 ~149 4 156 129 164 150 141 154 148 167 174 ~152 ~153 ~158 ~168 ~143 ~2 ~169 ~172 161 146 171 ~176 ~163 173 56 ~89 45 ~34 ~100 111 23 ~133 ~12 ~122 ~144 ~177 1 ~166
Altogether 96579+74594130 mems, 619697 bytes, 11038 nodes, 9803 clauses learned (ave 18.8->16.1), 148473 memcells.
(82 learned clauses were trivial.)
(893 learned clauses were discarded.)
(77 clauses were subsumed on-the-fly.)
(14 restarts.)

上記のような出力が得られれば,正しく設定されている.

2.2 Cプログラムのみ自分でコンパイルする

CWEBをインストールしたくない(あるいはできない)人のために, Cのソースプログラムに変換したものを以下に置く.

以下のようにダウンロード・展開・コンパイルをする.

$ cd ~/Desktop
$ mkdir taocp-sat
$ cd taocp-sat
$ curl -O http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/taocpsat-knuth.zip
$ unzip taocpsat-knuth.zip
$ cd knuth
$ chmod +x compile.sh
$ ./compile.sh

1行目でDesktopに移動している. 2行目でDesktop中に taocp-sat のフォルダが作成され,3行目でそのフォルダに移動する. 4行目で taocpsat-knuth.zip を取得し,5行目で展開,6行目で knuth フォルダに移動, 7行目でコンパイルしている.

taocp-sat/knuth 内には以下のディレクトリが作成される.

  • bin : コンパイル後の実行ファイル
  • pdf : PDFファイル
  • sat-examples/README : SAT examplesの説明
  • sat-examples/sources : SAT examplesのソース (SGBのソースを含む)
  • sat-life : SAT lifeのソース
  • sat-solvers : SATソルバーのソース
  • sgb : SGB (Stanford GraphBase)のソース

オリジナルのSAT examplesに含まれているベンチマーク問題は,容量節約のために削除している. 必要があれば,オリジナルをダウンロードすること.

コンパイルが成功すれば,以下のようにPATH環境変数を設定する.

$ echo 'export PATH=~/Desktop/taocp-sat/knuth/bin:$PATH' >>~/.profile
$ . ~/.profile

実行してみる.

$ sat13 -
Usage: sat13 [v<n>] [c<n>] [H<n>] [h<n>] [b<n>] [s<n>] [d<n>] [D<n>] [m<n>] [t<n>] [w<n>] [j<n>] [J<n>] [K<n>] [f<f>] [a<f>] [r<f>] [R<f>] [p<f>] [P<f>] [x<foo>] [l<bar>] [L<baz>] [z<poi>] [Z<poo>] [T<n>] < foo.sat

上記のような出力が得られれば,正しく設定されている.

2.3 コンパイル済みバイナリ

以下のようにコンパイル済みバイナリも用意している.

Mac OS Xの場合,以下のようにダウンロード・展開する.

$ cd ~/Desktop
$ mkdir taocp-sat
$ cd taocp-sat
$ curl -O http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/taocpsat-knuth-mac-bin.zip
$ unzip taocpsat-knuth-mac-bin.zip

Linuxの場合,以下のようにダウンロード・展開する.

$ cd ~/Desktop
$ mkdir taocp-sat
$ cd taocp-sat
$ curl -O http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/taocpsat-knuth-linux64-bin.zip
$ unzip taocpsat-knuth-linux64-bin.zip

含まれているファイルの内容,設定方法,動作の確認方法については,上記を参照のこと.

3 Knuth版プログラムの利用方法

詳細は,各々のPDFファイルを参照すること. 例えば sat13.pdf には以下の説明がある.

  • 1ページ: 入力の形式
    • 変数名はASCIIコードで "!" から "}" の間 (つまり16進で22から7Cまで)の8文字以内の文字列で, "~" から始まらないもの
    • 変数名の直前に "~" を付けると否定を表す
    • "~ " から始まる行はコメント
  • 3ページ: オプションの説明
    • sat-examples/README によれば,Knuthは以下のオプション指定を用いている.
      $ sat13 h14 b10000 T50000000000 <file.sat
      

まず,教科書4ページの式(6)に対して実行してみる.

  1. rivest-unsat.sat をダウンロードし, Desktop/taocp-sat 内に移動する.
  2. 以下のように実行する.
$ cd ~/Desktop/taocp-sat
$ sat13 <rivest-unsat.sat
(4 variables, 8 clauses, 24 literals successfully read)
~
UNSAT
Altogether 301+670 mems, 5804 bytes, 3 nodes, 3 clauses learned (ave 1.3->1.3), 60 memcells.
(2 clauses were subsumed on-the-fly.)
(1 restart.)
  • 充足不能を表す "~" 以外の行は,標準エラーに出力されている.
  • 出力中の最初の行は,入力中の変数の個数,節の個数,リテラルの個数を表している.
  • "301+670 mems" は,メモリーアクセス回数を表す. 301 が前処理でのアクセス数, 670 が解探索でのアクセス数である.
  • "5804 bytes" は,メモリー使用量を表す.
  • "3 nodes" は,解探索で暗黙的に作成された探索木のノード数を表す.
  • "3 clauses learned" は,学習節の個数を表す.
  • その他については,sat13.pdf中の説明や教科書中の説明を参照すること.

次に,教科書4ページの式(7) rivest-sat.sat に対しても同様に実行してみる.

$ sat13 <rivest-sat.sat
(4 variables, 7 clauses, 21 literals successfully read)
!SAT!
 3 ~1 2 4
Altogether 291+138 mems, 5752 bytes, 2 nodes, 0 clauses learned, 47 memcells.
(0 restarts.)
  • 解の値割当てを表す "3 ~1 2 4" 以外の行は,標準エラーに出力されている.

4 その他のプログラム

4.1 Scala版のプログラム

Scala版のプログラムなどは

としてまとめている. もちろん,Scalaがインストールされていることが必要である.

これらのプログラムは, Desktop/taocp-sat フォルダで展開して利用することを前提として作成してある. 例えば,以下のように展開する.

$ cd ~/Desktop/taocp-sat
$ curl -O http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/taocpsat-prog.zip
$ unzip taocpsat-prog.zip
$ cd prog
$ chmod +x taocpsat

Scalaのプログラムは最初にコンパイルする必要がある.

  • Scalaコンパイラを利用する場合,以下のようにする.
    $ mkdir target
    $ scalac -d target/taocpsat-1.0.jar src/main/scala/*.scala
    
  • sbtを利用する場合,以下のようにする (かなり時間がかかる).
    $ sbt package
    

以下が実行できればOKである.

$ ./taocpsat SolverA <rivest-sat.sat 
(4 variables, 7 clauses, 21 literals successfully read)
!SAT!
 ~1 2 ~3 4
Altogether 227+115 mems, 600 bytes, 3 nodes.

4.2 SATソルバー

代表的なCDCL型SATソルバーとしては,以下が挙げられる. いずれも,安定して優れた性能を示している.

特にSat4jはJava上で動くSATソルバーであり,様々な環境で簡単に利用できる. インストール方法は,以下の通り.

  1. http://www.sat4j.org の Products メニューを選択
  2. SAT4J SATの Download! をクリック
  3. sat4j satの2.3.4版である sat4j-sat4j-sat-v20130419.zip をクリック
  4. sat4j-sat4j-sat-v20130419.zip をダウンロードする
  5. zipファイルを展開し sat4j-sat.jar を取り出す

以下のようにして実行する.ただし「CNFファイル」はDIMACS CNF形式のファイルである.

$ java -jar sat4j-sat.jar CNFファイル名

Kunth版SATソルバーで用いている入力形式とDIMACS CNF形式の相互変換を行うプログラムも Knuth版プログラムに含まれている.

例えば,以下のように利用すれば良い.

$ sat-to-dimacs <rivest-sat.sat >/tmp/rivest-sat.cnf
(4 variables, 7 clauses, 21 literals successfully read)

$ java -jar sat4j-sat.jar /tmp/rivest-sat.cnf 
c SAT4J: a SATisfiability library for Java (c) 2004-2013 Artois University and CNRS
c This is free software under the dual EPL/GNU LGPL licenses.
c See www.sat4j.org for details.
c version 2.3.4.v20130419
c 7 constraints processed.
.....
s SATISFIABLE
v -1 2 3 4 0
c Total wall clock time (in seconds) : 0.038

Date:

Author: 神戸大学 情報基盤センター 田村直之

Org version 7.8.02 with Emacs version 26

Validate XHTML 1.0