Scarab チュートリアル

1. 参考資料
2. インストール (sbt)
3. 実行の方法
4. REPL による対話的な実行方法
- 4.1. CSP の定義
- 4.2. 解の探索
5. スクリプトファイルの読み込み
- 5.1. 練習問題
6. 例題集
7. その他 Scarab の説明とクラスとメソッドの簡単なまとめ

1 参考資料

Scarab 資料
- ホームページ
- github
プレゼンテーション
- Scarab の説明 @ ScalaMatsuri 2014
  - 日本語
  - 英語
- AIツールセミナー (2015年12月)
  - SAT型制約ソルバーと Scarab
  - alldiffrent制約を例に用いた制約の拡張
- SATソルバーの最新動向と利用技術 (日本語) @ PPL 2017
参考資料
- Copris による制約プログラミング入門 (本チュートリアルはこのページを参考にして作成しました).

2 インストール (sbt)

sbt 本家のインストールマニュアルをみて，sbt のインストールを行う. 以下の環境へのインストール方法が記載されている.
- Mac へのインストール方法
- Windows へのインストール方法
  - ただし，Windows に関しては sbt 本家サイトの方法だと環境変数の設定が必要になるので, パッケージ管理ソフト chocolatey を使うこの方法がおすすめ．
- Linux へのインストール方法
- 念のため, 上記のページを参考に Windows 10, Ubuntu 18.04, Mac OS X 10.11.6 にインストールした方法をここに記載する.
sbt-scarab.zip をダウンロードして適当なディレクトリに展開する．
sbt-scarab のディレクトリに入って sbt を実行すれば必要なライブラリ (scala を含む) のダウンロードとコンパイルが行われる (初回は結構時間がかかる)．
```
[sbt-scarab]$ sbt 
```

以下のように sbt:Scarab> というプロンプトが出てくる.

[sbt-scarab]$ sbt
[info] Loading settings from assembly.sbt ...
... 中略 ...
[info] sbt server started at 127.0.0.1:4891
sbt:Scarab>

以下のように console を実行する (初回は結構時間がかかる).
```
sbt:Scarab> console
```
以下のように scala というプロンプトが出てくれば sbt および scarab のインストール完了．
```
scala> 
```
:quit で終了できる．
```
scala> :quit
[sbt-scarab]$ 
```

3 実行の方法

Scarab の制約記述言語は Scala 上のドメイン特化言語として実装されている．Scala の説明
Scala と同じく3つの方法でプログラムを記述し，実行できる．
- REPL (Read Eval Print Loop) による対話的な実行方法
- スクリプトによるコンパイル不要な実行方法
- scalac で実行形式にコンパイルしてから実行する方法
- ブラウザで実行する
  - ここをクリックしてもらうだけで，少し待つと Jupyter notebooks 上の実行環境が表示されます．
  - 環境設定無しで, ブラウザだけで実行できます.
  - この仕組みは以下のリポジトリの binder/postBuild のフォーク (コピーです) を利用した Scarab4Binder で提供されます.
    - Almond Example
      - A collection of Jupyter notebooks showing what you can do with the Almond Scala kernel.
本チュートリアルでは REPL による対話的な実行方法を通して scarab を説明する．

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

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

問題の記述

12セント，16セント，20セント，27セントの切手をそれぞれ10枚持っている．

この時に90セント分の切手を構成できるか?

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

切手の問題の 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 (対話的な実行方法) で記述実行するために, sbt-scarab ディレクトリで sbt コマンド実行後に, console を実行する. すると最終的に scala> というコンソールが立ち上げる.

[sbt-scarab]$ sbt
sbt:Scarab> console
... メッセージ省略 ...
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 スクリプトファイルの読み込み

CSPをScalaのスクリプトファイルとして定義することもできる．
以下がCSPを定義したスクリプトファイルである.
- http://tsoh.org/scarab/sample-scripts/ex-csp.sc

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)

以下がCSPを定義した後に求解し，解があれば出力するスクリプトファイルである.
- http://tsoh.org/scarab/sample-scripts/ex-csp-solve.sc

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)

スクリプトファイルは以下のようにREPLから :load コマンドを使用して読み込む (カレントディレクトリにファイルがあるものとする)．

scala> :load ./ex-csp.sc
Loading ./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 ./ex-csp.sc
Loading ./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.1 練習問題

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 ./ex-subsetsum.sc
Loading ./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

練習問題
- 和が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)

練習問題
- n x n の魔方陣を記述してみよう．

6.3 ジョブショップスケジューリング問題

この問題は Fisher and Thompson 6x6 instance (ft06) を基に作成しました.

H. Fisher, G.L. Thompson (1963)

6つの製品 A, B, C, D, E, F をそれぞれ6つの工程 (オペレーション) を経て作る必要があります.

工程は使用する機械と処理時間で構成されます. 例えば製品Aは以下6つの工程を経て作られます.

工程1 (O1): 機械2を使って1時間

工程2 (O2): 機械0を使って3時間

工程3 (O3): 機械1を使って6時間

工程4 (O4): 機械3を使って7時間

工程5 (O5): 機械5を使って3時間

工程6 (O6): 機械4を使って6時間

各機械は同時に1つの製品しか処理することができません.

いま6つの製品 A, B, C, D, E, F の工程が以下のように与えられるとき, 全ての製品を作るために必要な最小の時間は何時間でしょうか?

製品	O1		O2		O3		O4		O5		O6
	機械	時間	機械	時間	機械	時間	機械	時間	機械	時間	機械	時間
A	2	1	0	3	1	6	3	7	5	3	4	6
B	1	8	2	5	4	10	5	10	0	10	3	4
C	2	5	3	4	5	8	0	9	1	1	4	7
D	1	5	0	5	2	5	3	3	4	8	5	9
E	2	9	1	3	4	5	5	4	0	3	3	1
F	1	3	3	3	5	9	0	10	4	4	2	1

この問題を CSP で表す方法はジョブ $i$ の工程 (オペレーション) $j$ が開始される時刻を整数変数 $stOp(i,j)$ とする方法である.
- James M. Crawford, Andrew B. Baker (1994)
Scarab プログラムでは, 以下のように記述できる. ここで $ops$ は, 上記の表を表している.

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

  /* 問題の定義 */
  val noJobs = 6
  val noMachines = 6
  val ops = Seq(
    Seq((2, 1), (0, 3), (1, 6), (3, 7), (5, 3), (4, 6)),
    Seq((1, 8), (2, 5), (4, 10), (5, 10), (0, 10), (3, 4)),
    Seq((2, 5), (3, 4), (5, 8), (0, 9), (1, 1), (4, 7)),
    Seq((1, 5), (0, 5), (2, 5), (3, 3), (4, 8), (5, 9)),
    Seq((2, 9), (1, 3), (4, 5), (5, 4), (0, 3), (3, 1)),
    Seq((1, 3), (3, 3), (5, 9), (0, 10), (4, 4), (2, 1)))

  /* makespan の素朴な下限値 */
  val lbMkSpan = ops.map(job => job.map(_._2).sum).max
  /* makespan の素朴な上限値 */
  val ubMkSpan = {
    for (m1 <- 0 until noMachines) yield {
      for (m2 <- 0 until noMachines) yield
        (0 until noJobs).map(ops(_)(m1)).filter(_._1 == m2).map(_._2).sum
    }.max
  }.sum

  int('makespan,lbMkSpan,ubMkSpan)


  /* 各オペレーションの開始時間を表す変数 */
  def lbSt(j: Int, n: Int) = ops(j).dropRight(noMachines - n).map(_._2).sum
  def ubSt(j: Int, n: Int) = ubMkSpan - ops(j).drop(n).map(_._2).sum
  val stOp =
    for (j <- 0 until noJobs) yield
      for (m <- 0 until noMachines) yield int('stOp(j,m), lbSt(j,m), ubSt(j,m))

  /* 各ジョブにおける各オペレーションの順序関係を表す制約 */
  for (j <- 0 until noJobs)
    for (m <- 0 until noMachines - 1)
      add(stOp(j)(m) + ops(j)(m)._2 <= stOp(j)(m+1))

  /* 各機械における競合関係を表す制約 */
  for (m <- 0 until noMachines) {
    val index4m =
      for (i <- 0 until noJobs; j <- 0 until noMachines if ops(i)(j)._1 == m)
        yield (i,j)
    for (i <- 0 until index4m.size; j <- i+1 until index4m.size) {
      val (i0,j0) = index4m(i)
      val (i1,j1) = index4m(j)
      add(stOp(i0)(j0) + ops(i0)(j0)._2 <= stOp(i1)(j1) ||
        stOp(i1)(j1) + ops(i1)(j1)._2 <= stOp(i0)(j0))
    }
  }

  /* 各ジョブが makespan 以内に終了することを表す制約 */
  for (i <- 0 until noJobs)
    add(stOp(i).last + ops(i).last._2 <= 'makespan)

  /* makespan の上限を制限する制約 */
  add('makespan <= ubMkSpan)

  /* 最適値を求めるための while 文 */
  var wm = ubMkSpan
  var sol: Option[Assignment] = None
  while(find) {
    val ub = (0 until noJobs).map{i => solution.intMap(stOp(i).last) + ops(i).last._2}.max
    wm = ub - 1
    sol = Some(solution)
    add('makespan <= wm)
  }

  println(s"optimum: ${wm+1}")
  for (i <- 0 until noJobs)
    println((0 until noMachines).map(j => sol.get(stOp(i)(j))).mkString(" "))

6.4 正方形矩形パッキング

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

最も素直なモデリングは整数変数 $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

  /* 大きい正方形のサイズを表す変数 */
  var lb = 15
  var ub = 100
  int('size, lb, ub)

  /* 各正方形の左下の座標を表す変数 */
  for (i <- 1 to n) {
    int('x(i),0,ub-i)
    int('y(i),0,ub-i)
  }

  /* 各正方形が大きい正方形の内側に詰め込まれることを表す制約 */
  for (i <- 1 to n)
    add(('x(i)+i <= 'size) && ('y(i)+i <= 'size))

  /* 各正方形が重ならないことを表す制約 */
  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 文 */
  add('size <= ub)
  while(find) {
    ub -= 1
    add('m <= ub)
  }
  println(s"optimum: ${ub+1}")

最適化部分は1ずつ下げているが，もっと良い方法がある．

6.5 その他の例題

ラングフォード・ペアリング
プログラム例は Scarab の Example ページにある．

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

7.1 jar ファイルとソースコード

scarab を jar ファイルにまとめたものです
scala -cp scarab-v196-s212.jar などどすることで, scarab を利用できます
使用している Scala のバージョンに応じて，以下から適切な scarab jar を選択してダウンロードしてください．
- (for Scala 2.12.*) use jars/scarab-v196-s212.jar
- (for Scala 2.11.*) use jars/scarab-v196-s211.jar
- (for Scala 2.10.*) use jars/scarab-v196-s210.jar
- ソースコードは Github から入手できます．

7.2 Scarab のクラスについて

Scarab のクラスについては scaladoc によって生成された API に詳しい.

代表的なものを以下に記述する．

クラス名	説明
CSP	制約充足問題 (CSP) のクラス
Assignment	CSP への値割当てのクラス
Solver	CSP ソルバーのクラス
Term	制約を構成する項を表す抽象クラス
Var	Term を継承する整数変数のクラス
Sum	Term を継承する項の和のクラス
Constraint	制約を表す抽象クラス
And	Constraint を継承するリテラルの連言のクラス
Or	Constraint を継承するリテラルの選言のクラス
Literal	Constraint を継承するリテラルのクラス
Bool	Literal を継承するブール変数のクラス
Not	Literal を継承するブール変数の否定のクラス
LeZero	Literal を継承する線形比較 $b + \sum_i a_ix_i \le 0$ のクラス
GeZero	Literal を継承する線形比較 $b + \sum_i a_ix_i \ge 0$ のクラス
EqZero	Literal を継承する線形比較 $b + \sum_i a_ix_i = 0$ のクラス
NeZero	Literal を継承する線形比較 $b + \sum_i a_ix_i \ne 0$ のクラス

これらのクラスに加えて, Scarab DSL でグローバル制約 alldiff を利用できるように以下のメソッドとして提供している (DSL ではトップレベルで利用できる).
- def alldiff(xs: Iterable[Term]): And
- def alldiff(xs: Term*): And

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

7.3 Scarab DSL について

CSP について
- Scarab DSL を呼んだ状態, すなわち以下のように import 文を書いた場合には, csp という名前のデフォルトの csp オブジェクトが定義されている.
```
scala> import jp.kobe_u.scarab._, dsl._
```
- この csp オブジェクトは以下のメソッドで編集できる.
  - 整数変数の追加
    - def int(x: Var, a: Int, b: Int): Var
    - def int(x: Var, d: Seq[Int]): Var
  - 制約の追加
    - def add(c: Constraint): Constraint
- これらのメソッドを呼ぶと, 暗黙的にデフォルトのオブジェクト csp に対する操作になる
```
scala> int('x, 1, 5)
res: jp.kobe_u.scarab.Var = x

scala> int('y, Seq(1,3,5))
res: jp.kobe_u.scarab.Var = y

scala> add('x + 'y >= 3)
res: jp.kobe_u.scarab.Constraint = GeZero(Sum(-3+x+y))

scala> csp
res: jp.kobe_u.scarab.CSP = CSP(Vector(x, y),Vector(),Map(x -> Domain(1 to 5), y -> Domain(1,3,5)),Vector(GeZero(Sum(-3+x+y))))
```
CSP における整数変数の定義について
- Scarab DSL では, 整数変数の定義が簡単に行えるようにシンボルの暗黙変換 (implicit conversion) を定義している.
- 以下は, 整数変数を通常の手続きで定義する方法である.
```
scala> import jp.kobe_u.scarab._, dsl._
import jp.kobe_u.scarab._
import dsl._

scala> Var("x","1","2")
res: jp.kobe_u.scarab.Var = x(1,2)
```
- ここで, x(1,2) はこの整数変数の変数名になる (変数名は重複があってはならない).
- Scala のシンボルはシングルクォーテーションを使って以下のように定義される.
```
scala> 's
res0: Symbol = 's
```
- 暗黙変換は, オブジェクトをシンボルと解釈すると, エラーになるが, CSPの整数変数と解釈するとうまくいく時に行われる.
- 以下は, そのような例である.
```
scala> 's(1)
res1: jp.kobe_u.scarab.Var = s(1)
```
- ここで 's(1) の 's~x をシンボルと解釈すると, シンボルは ~apply メソッド (Scala ではメソッド呼び出しの際に apply というメソッド名を省略可能) を持たないため，エラーとなる.
- しかし, Scarab DSL において, シンボルから整数変数オブジェクトへの暗黙変換が定義されているため, 's を整数変数として解釈することが試みられる．
- 結果として, 整数変数クラス (Var) が, apply メソッドを持ち, かつ Int 型の引数を取ることが出来るため (実際はより幅広く任意個の Any 型を引数に取れる), 's は Var 型のオブジェクトと解釈され, 's(1) は Var 型のオブジェクトのメソッド apply を引数 1 に対して呼んだと解釈される.
- Var 型の apply メソッドは, ’s に引数1を追加した新しい Var 型のオブジェクトを生成するファクトリメソッドになっているので, 最終的に s(1) という名前の整数変数が返される.
- 以下は, Var 型オブジェクトを生成するいくつかの方法である.
```
scala> 's(1,2)
res2: jp.kobe_u.scarab.Var = s(1,2)

scala> 's(1)(2)
res3: jp.kobe_u.scarab.Var = s(1,2)

scala> 's(1)(2)(3)
res4: jp.kobe_u.scarab.Var = s(1,2,3)

scala> 's(1,2,3)
res5: jp.kobe_u.scarab.Var = s(1,2,3)
```
- ’s(1,2) と ’s(1)(2) の結果は同じになる．
  - ’s(1,2) は, apply メソッドを2個の引数で呼んでいる
  - ’s(1)(2) は, ’s(1) で生成されるオブジェクトに対してさらに apply メソッドを呼んでいる.

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

V, T, C, B を Var (整数変数), Term (項), Constraint (制約), Bool (ブール変数) に対応するScarabオブジェクトとする.
Int, String, Any は Scala のオブジェクトとする．
制約に関する Scarab DSL の構文は BNF 記法を用いて以下のように定義される．

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.5 プログラムの簡単なまとめ

項オブジェクト (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オブジェクトに暗黙変換される．
```
pscala> '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)
```
制約オブジェクト
- Termオブジェクトと比較演算子 <= ($\le$), <, >= ($\ge$), >, = ($=$),　!== ($\ne$) の組合せで構成される．
```
scala> Sum('x - 'y) <= 3
res25: jp.kobe_u.scarab.Constraint = LeZero(Sum(-3+x-y))
```
- 宣言されると同時に <= 0 の形に正規化される．
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))
```
解の探索
- 最初の解の探索は 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の解に復号化
その他
- 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

	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

Scarab チュートリアル

Table of Contents

1 参考資料

2 インストール (sbt)

3 実行の方法

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

4.1 CSP の定義

4.2 解の探索

5 スクリプトファイルの読み込み

5.1 練習問題

6 例題集

6.1 部分和問題

6.2 魔方陣

6.3 ジョブショップスケジューリング問題

6.4 正方形矩形パッキング

6.5 その他の例題

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

7.1 jar ファイルとソースコード

7.2 Scarab のクラスについて

7.3 Scarab DSL について

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

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