Scarab チュートリアル

Table of Contents

1 参考資料

2 インストール

以下の説明は Scarab のインストールの説明です.

  1. Java runtime version 1.8 以降をインストールする.
  2. Scala をインストールしてください (2019年2月時点で 2.12.8 が最新).
  3. 使用している Scala のバージョンに応じて,以下から適切な scarab jar を選択してダウンローそしてください.

以下このチュートリアルでは次のようなディレクトリ構成になっていると仮定しています.

csp/
 |
 |- scarab-<scarab version>-<scala version>.jar
  • 適当なディレクトリに移動します (例えば sat-tools).
$ mkdir csp
$ cd csp
$ mkdir classes
$ wget http://tsoh.org/scarab/jars/scarab-v196-s212.jar

3 実行の方法

  • Scarab の制約記述言語は Scala 上のドメイン特化言語として実装されて います. Scala の説明
  • Scala と同じく3つの方法でプログラムを記述し,実行できます.
    • REPL (Read Eval Print Loop) による対話的な実行方法
    • スクリプトによるコンパイル不要な実行方法
    • scalac で実行形式にコンパイルしてから実行する方法
  • 以下ではまずREPL による対話的な実行方法を通して scarab に慣れていきたいと思います.

4 REPL による対話的な実行方法

簡単な例題を通して, Scala の REPL (対話的実行環境) を用いた scarab の 利用方法を理解しよう.

(問題)
12セント,16セント,20セント,27セントの切手をそれぞれ10枚持っている.
この時に90セント分の切手を構成できるか?

この問題は以下の制約充足問題 (CSP) として定義できる.

  • 変数の集合 \(X = \{a, b, c, d\}\)
  • 変数が取り得る値の集合 (ドメイン) を表す関数 \(Dom\)
    • \(Dom(a) = \{0, \ldots, 10\}\)
    • \(Dom(b) = \{0, \ldots, 10\}\)
    • \(Dom(c) = \{0, \ldots, 10\}\)
    • \(Dom(d) = \{0, \ldots, 10\}\)
  • 制約条件 \(C\)
    • \(12a + 16b + 20c + 27d = 90\)

4.1 CSP の定義

  • 上記のCSPに対応するScarabプログラムは以下になります.
import jp.kobe_u.scarab._ , dsl._

int('a, 0, 10)
int('b, 0, 10)
int('c, 0, 10)
int('d, 0, 10)

add('a * 12 + 'b * 16 + 'c * 20 + 'd * 27 === 90)
  • まず REPL を用いた対話的な実行方法を説明します.“scala -cp scarab-v196-s212.jar” と入力します.

    hoge $ scala -cp {{{scarabJAR()}}} 
    Welcome to Scala version 2.11.5 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.1_11).
    Type in expressions to have them evaluated.
    Type :help for more information.
    
    scala>
    
    • scala の REPL モードが scarab のクラスを読み込んで起動されます.
    • 次に scarab のクラスをインポートします.

      scala> import jp.kobe_u.scarab._ , dsl._
      import jp.kobe_u.scarab._
      import dsl._
      
    • import 文が読み込まれ (Read Eval) 実行結果が表示 (Print) されます.
    • 整数変数を定義します.

      scala> int('a, 0, 10)
      res0: jp.kobe_u.scarab.Var = a
      
      scala> int('b, 0, 10)
      res1: jp.kobe_u.scarab.Var = b
      
      scala> int('c, 0, 10)
      res2: jp.kobe_u.scarab.Var = c
      
      scala> int('d, 0, 10)
      res3: jp.kobe_u.scarab.Var = d
      
    • ここでは変数a, b, c, dを宣言しています (下限 0,上限 10). シングルクォーテーションから始まる記述 ’x は ScalaにおけるSymbolオブジェクトの記法ですが, Scarab DSLによりScarabの整数変数 (Varオブジェクト)に暗黙変換されます.
    • 制約を定義します.

      scala> add('a * 12 + 'b * 16 + 'c * 20 + 'd * 27 === 90)
      res4: jp.kobe_u.scarab.Constraint = EqZero(Sum(-90+12*a+16*b+20*c+27*d))
      
    • ここでは制約 12a + 16b + 20c + 27d = 90 を追加しています.
      • add は制約をCSPオブジェクトに追加するためのメソッドです.
      • 制約中での等号に \(===\) を用いる点に注意してください.
      • 5 * ’a のように係数を前にして記述できない点に注意してください.
    • 定義したCSPオブジェクトは変数cspとして参照できます.

      scala> csp
      res8: jp.kobe_u.scarab.CSP = CSP(Vector(a, b, c, d),Vector(),Map(..),Vector(..))
      
    • CSPオブジェクトは,整数変数の列 variables, ブール変数の列 bools, 変数ドメインのマップ dom, 制約の列 constraints から構成されます.
    • 以下のように csp オブジェクトから参照できます.

      scala> csp.variables
      res5: IndexedSeq[jp.kobe_u.scarab.Var] = Vector(a, b, c, d)
      
      scala> csp.constraints
      res6: IndexedSeq[jp.kobe_u.scarab.Constraint] = Vector(EqZero(Sum(-90+12*a+16*b+20*c+27*d)))
      
    • show メソッドでも表示できる.

      scala> csp.show
      int(a,Domain(0 to 10))
      int(b,Domain(0 to 10))
      int(c,Domain(0 to 10))
      int(d,Domain(0 to 10))
      EqZero(Sum(-90+12*a+16*b+20*c+27*d))
      
    • CSPオブジェクトは,変数や制約の追加を行える mutable なオブジェクトとして実装されている.

4.2 解の探索

  • 最初の解の探索は find で行う.

    scala> find
    res9: Boolean = true
    
  • 結果の true は,解が存在することを表す. CSPの解は,solution 変数 に代入されている.

    scala> solution
    res10: jp.kobe_u.scarab.Assignment = Assignment(Map(a -> 3, b -> 0, c -> 0, d -> 2),Map())
    
  • Solutionオブジェクトは,整数変数 (Varオブジェクト)に対する値割当てを表すマップと ブール変数 (Boolオブジェクト)に対する値割当てを表すマップから構成される.

    scala> solution.intMap
    res11: Map[jp.kobe_u.scarab.Var,Int] = Map(a -> 3, b -> 0, c -> 0, d -> 2)
    
    scala> solution.boolMap
    res12: Map[jp.kobe_u.scarab.Bool,Boolean] = Map()
    
  • 解における各変数の値は solution メソッドで得ることができる.

    scala> solution('a)
    res13: Int = 3
    
    scala> solution('b)
    res14: Int = 0
    
    scala> solution('c)
    res15: Int = 0
    
    scala> solution('d)
    res16: Int = 2
    
  • 次の解の探索は findNext で行う.

    scala> findNext
    res17: Boolean = true
    
    scala> solution
    res18: jp.kobe_u.scarab.Assignment = Assignment(Map(a -> 0, b -> 1, c -> 1, d -> 2),Map())
    
  • findNext は最も最近得られた解の否定をcspに追加することで次の解を求めている.
  • show メソッドを実行すると,制約が追加されていることが分かる.

    int(a,Domain(0 to 10))
    int(b,Domain(0 to 10))
    int(c,Domain(0 to 10))
    int(d,Domain(0 to 10))
    LeZero(Sum(-90+12*a+16*b+20*c+27*d))
    LeZero(Sum(90-12*a-16*b-20*c-27*d))
    Or(LeZero(Sum(-2+a)),LeZero(Sum(4-a)),LeZero(Sum(1+b)),LeZero(Sum(1-b)),LeZero(Sum(1+c)),LeZero(Sum(1-c)),LeZero(Sum(-1+d)),LeZero(Sum(3-d)))
    
  • ここでこの次の解の探索時には,最初に解を求めた時の学習節を再利用するインクリメンタルSAT解法を行っている.
  • Scarab では明示的にSATソルバーを reset しない限り,常に学習節を保持して効率的に求解を行う.
  • もう一度 findNext を呼ぶと false が返る.

    scala> findNext
    res22: Boolean = false
    
  • 結果の false は,解が存在しないことを表す. この場合,変数 solution は null になっている.

    scala> solution
    res23: jp.kobe_u.scarab.Assignment = null
    

5 スクリプトによるコンパイル不要な実行方法

5.1 内容の確認

import jp.kobe_u.scarab._ , dsl._

int('a, 0, 10)
int('b, 0, 10)
int('c, 0, 10)
int('d, 0, 10)
add('a * 12 + 'b * 16 + 'c * 20 + 'd * 27 === 90)
import jp.kobe_u.scarab._ , dsl._

int('a, 0, 10)
int('b, 0, 10)
int('c, 0, 10)
int('d, 0, 10)
add('a * 12 + 'b * 16 + 'c * 20 + 'd * 27 === 90)

if (find) println(solution)

5.2 scala コマンドによる実行

  • 以下のように保存したファイルを scala コマンドに与えればコンパイル無しで実行してくれる.
$ scala -cp scarab-v196-s212.jar ex-csp-solve.sc

5.3 REPLからのスクリプトファイルの読み込み

  • スクリプトファイルは以下のようにREPLから :load コマンドを使用して読み込む.
scala> :load ./csp/files/ex-csp.sc
Loading ./csp/files/ex-csp.sc...
import jp.kobe_u.scarab._
import dsl._
res0: jp.kobe_u.scarab.Var = a
res1: jp.kobe_u.scarab.Var = b
res2: jp.kobe_u.scarab.Var = c
res3: jp.kobe_u.scarab.Var = d
res4: jp.kobe_u.scarab.Constraint = EqZero(Sum(-90+12*a+16*b+20*c+27*d))
  • スクリプトファイルの内容を変更した後,再度読み込みたい場合には,:load の前に reset (scarab のコマンド) を実行し,いったんCSPの定義を消去する必要がある.
scala> reset

scala> :load ./files/ex-csp.sc
Loading ./files/ex-csp.sc...
import jp.kobe_u.scarab._
import dsl._
res13: jp.kobe_u.scarab.Var = a
res14: jp.kobe_u.scarab.Var = b
res15: jp.kobe_u.scarab.Var = c
res16: jp.kobe_u.scarab.Var = d
res17: jp.kobe_u.scarab.Constraint = EqZero(Sum(-90+12*a+16*b+20*c+27*d))

5.4 練習問題

  • 89円分の切手を構成できるかテストしてみよう.

6 簡単な例題

6.1 部分和問題

使いきらなければならない予算が 50 千円あります.
購入できる品物は 2, 3, 5, 8, 13, 21, 34 (単位: 千円) が1つずつです.
ちょうど予算を使い切るような組合せはあるか?
  • この問題は 部分和問題 (Subset sum problem)として知られている問題の例である. 部分和問題はNP-完全である (Wikipedia:部分和問題).
  • これは,以下の制約充足問題として定式化できる.

    • \(X = \{x_2, x_3, x_5, x_8, x_{13}, x_{21}, x_{34}\}\)
    • \(Dom\)
      • \(Dom(x_2) = \{0, 1\}\)
      • \(Dom(x_3) = \{0, 1\}\)
      • \(Dom(x_5) = \{0, 1\}\)
      • \(Dom(x_8) = \{0, 1\}\)
      • \(Dom(x_{13}) = \{0, 1\}\)
      • \(Dom(x_{21}) = \{0, 1\}\)
      • \(Dom(x_{34}) = \{0, 1\}\)
    • \(C\)
      • \(2x_2 + 3x_3 + 5x_5 + 8x_8 + 13x_{13} + 21x_{21} + 34x_{34} = 50\)
  • CSPを記述したファイルは以下のようになる ex-subsetsum.sc
import jp.kobe_u.scarab._ , dsl._ 

def define(sum: Int) {
  reset
  boolInt('x(2))
  boolInt('x(3))
  boolInt('x(5))
  boolInt('x(8))
  boolInt('x(13))
  boolInt('x(21))
  boolInt('x(34))
  add('x(2)*2 + 'x(3)*3 + 'x(5)*5 + 'x(8)*8 + 'x(13)*13 + 'x(21)*21 + 'x(34)*34 === sum)
}
  • boolInt は 0-1 変数の宣言であり, boolInt(x) は int(x, 0, 1) と同一である.
  • また上記プログラムでは,直接CSPを記述するのではなく, 関数 define(sum: Int) で和を与えられるようにしている. この場合,利用方法は以下のようになる.
scala> :load ./files/ex-subsetsum.sc
Loading ./files/ex-subsetsum.sc...
import jp.kobe_u.scarab._
import dsl._
define: (sum: Int)Unit

scala> define(50)

scala> find
res1: Boolean = true

scala> solution
res2: jp.kobe_u.scarab.Assignment = Assignment(Map(x(8) -> 1, x(21) -> 1, x(3) -> 1, x(13) -> 1, x(2) -> 0, x(34) -> 0, x(5) -> 1),Map())
  • 解が見にくいが,以下のようにすれば見やすくなる.
scala> for (x <- csp.variables) println(s"$x ${solution(x)}")
x(2) 0
x(3) 1
x(5) 1
x(8) 1
x(13) 1
x(21) 1
x(34) 0
  • この解は 3, 5, 8, 13, 21 (単位: 千円) の品物を買えば 50 千円になることを表している.
  • 34 千円の品物が入った解が欲しい場合は,以下のように制約を追加して解を求めれば良い.
scala> add('x(34) === 1)
res6: jp.kobe_u.scarab.Constraint = EqZero(Sum(-1+x(34)))

scala> find
res7: Boolean = true

scala> solution
res8: jp.kobe_u.scarab.Assignment = Assignment(Map(x(8) -> 0, x(21) -> 0, x(3) -> 1, x(13) -> 1, x(2) -> 0, x(34) -> 1, x(5) -> 0),Map())

scala> for (x <- csp.variables) println(s"$x ${solution(x)}")
x(2) 0
x(3) 1
x(5) 0
x(8) 0
x(13) 1
x(21) 0
x(34) 1
  1. 練習問題
    • 和が40の場合はどうなるか?

6.2 魔方陣

1から9の数字を 3×3 に配置し, 各行,各列,各対角線の和がいずれも15になるようにせよ.
  • このような配置は魔方陣 (Magic square)と呼ばれる (Wikipedia:魔方陣).
  • 以下のようにCSPとして定式化できる.
  • \(X = \cup_{0 \le i,j \le 2} x_{i,j} \)
    • \(x_{0,0}, x_{0,1}, \ldots, x_{2,2}\)
  • \(Dom\)
    • \(Dom(x_{i,j}) = \{1, 9\}\)
  • \(C\)
    • \(alldiff(x_{0,0}, x_{0,1}, \ldots, x_{2,2})\)
    • \( x_{i,0} + x_{i,1} + x_{i,2} = 15 (i = 0, 1, 2) \)
    • \( x_{0,j} + x_{1,j} + x_{2,j} = 15 (j = 0, 1, 2) \)
    • \( x_{0,0} + x_{1,1} + x_{2,2} = 15 \)
    • \( x_{0,2} + x_{1,1} + x_{2,0} = 15 \)
  • ここで alldiff はCSPのグローバル制約の一つ Alldifferent 制約であり,与えられた引数が互いに異なることを表す.
  • すなわち alldiff(\(x_1, x_2, \ldots, x_n\)) は \(x_i \ne x_j\) (for all \(i < j\)) と同じである.
  • CSPを記述したファイルは以下のようになる ex-magicsq.sc
import jp.kobe_u.scarab._ , dsl._

reset
int('x(0,0), 1, 9); int('x(0,1), 1, 9); int('x(0,2), 1, 9)
int('x(1,0), 1, 9); int('x(1,1), 1, 9); int('x(1,2), 1, 9)
int('x(2,0), 1, 9); int('x(2,1), 1, 9); int('x(2,2), 1, 9)
add(alldiff(
  'x(0,0), 'x(0,1), 'x(0,2),
  'x(1,0), 'x(1,1), 'x(1,2),
  'x(2,0), 'x(2,1), 'x(2,2)
))
add('x(0,0) + 'x(0,1) + 'x(0,2) === 15)
add('x(1,0) + 'x(1,1) + 'x(1,2) === 15)
add('x(2,0) + 'x(2,1) + 'x(2,2) === 15)
add('x(0,0) + 'x(1,0) + 'x(2,0) === 15)
add('x(0,1) + 'x(1,1) + 'x(2,1) === 15)
add('x(0,2) + 'x(1,2) + 'x(2,2) === 15)
add('x(0,0) + 'x(1,1) + 'x(2,2) === 15)
add('x(0,2) + 'x(1,1) + 'x(2,0) === 15)
  • ただこの書き方だともっと大きい魔方陣のプログラムを書くのは大変.
  • Scala の制御構造やクラスを利用すればもっと以下のように簡潔に記述できる.
import jp.kobe_u.scarab._, dsl._

val xs = for (i <- 1 to 3; j <- 1 to 3) yield int('x(i,j), 1, 9)
add(alldiff(xs))

for (i <- 1 to 3)
  add(Sum((1 to 3).map(j => 'x(i,j))) === 15)
for (j <- 1 to 3)
  add(Sum((1 to 3).map(i => 'x(i,j))) === 15)

add(Sum((1 to 3).map(i => 'x(i,i))) === 15)
add(Sum((1 to 3).map(i => 'x(i,4-i))) === 15)
  1. 練習問題
    • n x n の魔方陣を記述してみよう.

6.3 正方形矩形パッキング

正方形詰込み問題 SP(n,s) は一辺の長さ 1 から n まで1ずつ増加する正方形の集合を
一辺の長さ s の正方形の枠内に重なりなく配置する問題である.

spp15.png

  • 最も素直なモデリングは整数変数 \(x_{i}, y_{i} \in \{0, \ldots, s-i\}\) をそれぞれの正方形 \(i~(1 \le i \le n)\) に \((x_{i},~y_{i})\) が正方形 \(i\) の左下の座標を指すようにするものである.
  • 以下の制約は任意の二つの正方形 \(i\) と \(j\) (但し \(1\le i < j \le n\)) が重なることを禁止する.
    • \((x_{i}+i \le x_{j}) \vee (x_{j}+j \le x_{i}) \vee (y_{i}+i \le y_{j}) \vee (y_{j}+j \le y_{i})\)
import jp.kobe_u.scarab._ , dsl._

val n = 15
val s = 100

var lb = 15
var ub = s
int('m, lb, ub)

for (i <- 1 to n) { 
  int('x(i),0,s-i) 
  int('y(i),0,s-i) 
}

for (i <- 1 to n)
  add(('x(i)+i <= 'm) && ('y(i)+i <= 'm)) 

for (i <- 1 to n; j <- i+1 to n) 
  add(('x(i)+i<='x(j)) || ('x(j)+j<='x(i)) || ('y(i)+i<='y(j)) || ('y(j)+j<='y(i)))

while(lb <= ub && find('m <= ub)) {
  add('m <= ub)
  ub -= 1
  println(ub)
}
  • 最適化部分は1ずつ下げているが,もっと良い方法がある.

6.4 その他の例題

7 Scarab のクラスとメソッドの簡単なまとめ

7.1 Scarab DSL の制約記述に関する構文 (BNF記法)

  • V, T, C, BVar (整数変数), Term (項), Constraint (制約), Bool (ブール変数) に対応するScarabオブジェクトとする.
  • Int, String, Any は Scala のオブジェクトとする.
  • 制約に関する Scarab DSL の構文は以下のように定義される.
T  ::= V | -T | T + Int | T + T | T - Int | T - T | T * Int | Sum(V, ...) | Sum(Seq(V, ...))  
V  ::= Var(String, String, ...) | V(Any, ...)
C  ::= B | T op T | !C | C && C | C || C | alldiff(Seq(T, ...)) |  
      And(C, ...) | And(Seq(C, ...)) | Or(C, ...) | Or(Seq(C, ...))
op ::= <= | < | => | > | === | !==
B  ::= Bool(String, String, ...) | B(Any, ...)

7.2 Scarab のクラス図

  1. CSPに関係するクラス図

    class_diagram_csp.png

  2. 制約ソルバーに関係するクラス図

    class_diagram_solver.png

7.3 プログラムの簡単なまとめ

  1. 項オブジェクト (Termオブジェクト)
    1. 整数変数オブジェクト (Varオブジェクト)
      • 整数変数オプジェクトは Var で生成する. 引数にはその名前を与える.
      scala> val x = Var("x")
      x: jp.kobe_u.scarab.Var = x
      
      • 名前がない場合は,新しい匿名変数オブジェクトが生成される.
      scala> val z = Var()
      z: jp.kobe_u.scarab.Var = TMP_I_1
      
      • Varオブジェクトに添字を与えることで,新しいVarオブジェクトを生成できる. 添字には整数や文字列を使用でき,また複数与えても良い. ただし,添字にScarabの整数変数を用いることはできない.
      scala> x("book", "apple", 300)
      res16: jp.kobe_u.scarab.Var = x(book,apple,300)
      
      • Scala の Symbol は,Varオブジェクトに暗黙変換される.
      scala> 'abc(2)
      res19: jp.kobe_u.scarab.Var = abc(2)
      
      • Varオブジェクトは後述の項 (Term) オブジェクトの一種である.
    2. 和算オブジェクト (Sumオブジェクト)
      • Sumオブジェクトは整数変数の加算 (\(+\)),減算 (\(-\)) を表す.
      scala> Sum('x + 'y)
      res21: jp.kobe_u.scarab.Sum = Sum(+x+y)
      
      scala> Sum(- 'x - 'y)
      res22: jp.kobe_u.scarab.Sum = Sum(-x-y)
      
      scala> - Sum(- 'x - 'y)
      res23: jp.kobe_u.scarab.Sum = Sum(+x+y)
      
  2. 制約オブジェクト
    • Termオブジェクトと比較演算子 <= (\(\le\)), <, >= (\(\ge\)), >, = (\(=\)), !== (\(\ne\)) の組合せで構成される.
    scala> Sum('x - 'y) <= 3
    res25: jp.kobe_u.scarab.Constraint = LeZero(Sum(-3+x-y))
    
    • 宣言されると同時に <= 0 の形に正規化される.
  3. CSPオブジェクト
    • CSPオブジェクトは,制約充足問題を表すオブジェクトである. jp.kobe_u.scarab.dsl._ を import した場合, デフォールトのCSPオブジェクトを変数 csp として参照できる.
    1. 整数変数の宣言 (CSPへ整数変数を追加)
      • 整数変数は int メソッドで宣言する. 通常は,下限値と上限値を与える.
      scala> int('x, 0, 10)
      res27: jp.kobe_u.scarab.Var = x
      
      • 飛び飛びのドメインも利用できる.
      scala> int('y, Seq(1,3,5))
      res28: jp.kobe_u.scarab.Var = y
      
      • 変数のドメインは,csp.dom メソッドで確認できる.
      scala> csp.dom('x)
      res29: jp.kobe_u.scarab.Domain = Domain(0 to 10)
      
      scala> csp.dom('y)
      res30: jp.kobe_u.scarab.Domain = Domain(1,3,5)
      
    2. 制約の追加
      • 制約の追加は add メソッドで宣言する.
      scala> add('x === 'y * 2)
      res31: jp.kobe_u.scarab.Constraint = EqZero(Sum(+x-2*y))
      
      • 現時点での変数宣言と制約は show で確認できる.
      scala> show
      int(x,Domain(0 to 10))
      int(y,Domain(1,3,5))
      EqZero(Sum(+x-2*y))
      
  4. 解の探索
    • 最初の解の探索は find で行う.
    scala> find
    res34: Boolean = true
    
    • 結果が true なら解が存在し,false なら存在しない. 見つかった解は solution で表示される.
    scala> solution
    res35: jp.kobe_u.scarab.Assignment = Assignment(Map(x -> 10, y -> 5),Map())
    
    • 変数を solution への引数として与えれば,値が得られる.
    scala> solution('x)
    res37: Int = 10
    
    • find メソッド中では,以下が実行されている.
      • CSPオブジェクトをSAT符号化し,SATソルバーへ節を追加
      • SATソルバーによる解探索を実行
      • SATソルバーが発見した解をCSPの解に復号化
    • 次の解は findNext で求める.
    scala> findNext
    res38: Boolean = true
    
    scala> solution
    res39: jp.kobe_u.scarab.Assignment = Assignment(Map(x -> 6, y -> 3),Map())
    
    • findNextメソッド中では,以下が実行されている.
      • 現在の解の否定を表す条件をソルバーに追加
      • 追加したCNFに対し,SATソルバーによる解探索を実行
      • SATソルバーの発見した解をCSPの解に復号化
  5. その他
    • SATソルバーを切り替えるには以下のようにする
    use(new Sat4jPB)
    use(new ExtSatSolver("minisat"))
    
    • 外部SATソルバー (ExtSatSolver) の引数には実行パスを入れる.
    • エンコーダを切り替えるには以下のようにする
      • デフォルトは OrderEncoder
    use(new NativePBEncoder(csp, satSolver))
    use(new LogEncoder(csp, satSolver))
    
    • 各種符号化・機能とSatSolverの対応表は以下になる.
      Sat4j Sat4jPB ExtSolver
    OrderEncoder o o o
    LogEncorder o o x
    NativePBEncoder o o x
    インクリメンタルSAT o o x
    仮説 o o x
    極小非充足コア o x x

Author: Takehide Soh

Created: 2019-02-11 月 16:59

Validate