MAGE Vol.34, No.42 (2014.7)【研究報告】

Scala 上で実現された SAT 型制約プログラミングシステム∗
宋 剛秀 1
共同研究者
番原 睦則 1 田村 直之 1
Daniel Le Berre2 Stéphanie Roussel2
1 神戸大学 情報基盤センター 学術情報処理研究部門
2 CRIL-CNRS, UMR 8188, Université d’Artois

はじめに

1

命題論理の充足可能性判定 (SAT; propositional satisfiability) 問題は計算理論において中心的であり，また人工知能や計算機科学の分野においても重要な問題である [3, 8]. 2000 年以降 SAT 問題を解くためのプログラムである SAT ソルバーの性能が飛躍的に向上しており [15]，このような性能向上は与えられた問題を SAT 問題に符号化し，SAT ソルバーを用いて解を求める SAT 型システムの開発を促進してきた．これまで論理合成，プランニング，スケジューリング，ハードウェア・
ソフトウェアの検証などで SAT 型システムが成功をおさめている [8, 2, 26, 14]．
SAT 型システムは効果的な方法であるが，与えられた問題に対して提案した解法を毎回はじめから実装するのは効率が悪い．そこで制約充足問題 (CSP; constraint satisfaction problem) などの汎用的な形式で問題を記述して解くことができる SAT 型制約プログラミングシステムが開発されてきた [24, 27, 7, 13, 32]．例えば Sugar[24] は専用の制約言語で制約充足問題 (CSP; constraint
satisfaction problem) を記述し，順序符号化 [23] によって SAT 問題へと符号化した後に SAT ソル
バーによって解を求める SAT 型制約プログラミングシステムである．2008 年と 2009 年に CSP ソ
ルバー競技会 [11] のグローバル制約部門で優勝し，また近年では 2013 年にパッキング配列の最良解を更新するのに用いられた [16]．Sugar は専用の記述言語を用いることでユーザにとって理解し易い制約表現を可能にしているが，一方でループなどの汎用プログラミング言語で提供されている制御構造を扱うことができない．また SAT ソルバーとの連携はファイルを介して外部プロセスを起動することによって行なうなど SAT ソルバーをブラックボックスとして扱っている．これはいろ
いろな種類の SAT ソルバーをコストをかけずに切り替えることが可能であり，利点の一つでもあるが SAT ソルバー内部の低レベル機能の利用と拡張には対応することが難しくなる．
本稿では汎用プログラミング言語である Scala 上で実装された SAT 型制約プログラミングシス
テムである Scarab1 を紹介する．Scarab は，制約プログラミングのためのドメイン特化言語 (DSL;
Domain-specific Language) である Scarab DSL, SAT 符号化モジュール，そしてバックエンドのSAT ソルバーへのインターフェースから構成される．現在，Scarab では SAT 符号化として順序符
号化 [23] ，SAT ソルバーには Sat4j[10] を利用可能である．
Scarab の設計方針は SAT 型システム開発者に表現性，効率性，変更性，可搬性を備えたワーク
ベンチを提供することである．
表現性:
∗
1

ScarabDSL と Scala の両方を用いて与えられた問題を記述することが可能である．

本稿は共同研究者と執筆した論文 [21, 19, 20] を基にして作成した．
http://kix.istc.kobe-u.ac.jp/~soh/scarab/

42

MAGE Vol.34, No.42 (2014.7)

CSP

SAT 符号化

オブジェクト

SAT

オブジェクトScarab
プログラム

Sat4j

MAP

(DSL+Scala)

CSPの解Scarab DSL

逆符号化
CSP ソルバー API

SATの解

SAT ソルバー API

図 1. Scarab の構成

効率性: Scarab は最適化された順序符号化法を用いているという点で効率的である [23]．順序符号
化は 2008 年，2009 年に CSP ソルバー競技会のグローバル部門で優勝した Sugar[24] に採用されている．
変更性: Scarab では SAT 型システム開発者が自前の制約を定義し，変更・改良することが可能である．また Scarab のソースコードは全体で 500 行ほどであり，Scarab 本体の変更も可能である．
可搬性:

Scarab と Sat4j は両方とも JVM 上で動作し，可搬性のあるシステムを実現可能である．

図 1 に Scarab の構成図を示す．まず SAT 型システム開発者が Scala と Scarab DSL を用いて記述したプログラム (Scarab プログラム) によって CSP オブジェクトが生成される．次に Scarab プ
ログラムによって CSP ソルバーが求解のために API を通して呼ばれた時に，CSP オブジェクトはSAT オブジェクトへと変換される．続いて CSP ソルバーから SAT ソルバー Sat4j が API を通して実行される．解が存在すれば逆符号化を通して CSP の解が返される．
汎用プログラミング言語を制約記述に用いる SAT 型制約プログラミングシステムの従来研究として Copris (in Scala) [27], Numberjack (in Python) [7], Bee (in Prolog) [13], B-Prolog (in Prolog)[32] が挙げられる．この中でも, 著者らが開発した Copris は Scala 上の埋込み DSL を備えている
点で Scarab と同様のツールである．Copris では Sugar を SAT 符号化モジュールとして用いており，
SAT ソルバーを外部プロセスとして起動するなど SAT ソルバーとの連携は疎に行われる．一方，
Scarab は，SAT 符号化，SAT ソルバーのグラスボックス化を設計方針としており，SAT 符号化モジュールを含めて Scala 上で 1000 行程度で実装されている．これによりコードはコンパクトで変更容易であり，新しいアイデアを実験し易い．また SAT ソルバーとの密な連携によりインクリメンタ
ル解法や組込み制約など SAT ソルバーの低レベル機能の利用ができる点，それらを Scala 上で拡張できる点において Copris と異なるなるツールになっている．
以下では 2 節で Scarab の入力にあたる Scarab プログラムを説明する．3 節ではと三つの問題記
述例を説明する．次に 4 節では Scarab の特長である Sat4j を用いた高度な解法について説明を行う，
5 節では性能評価を示す．

2

Scarab プログラム

Scarab を利用するための最も基本的な方法は Scarab プログラムを記述することである．Scarab
プログラムの記述には Scala と制約プログラミングのための DSL である Scarab DSL の両方を利用可能である．本節では Scala と Scarab DSL を説明した後，二つの問題記述例を通して Scarab の基
本的機能の説明を行う.

43

MAGE Vol.34, No.42 (2014.7)

T ::= V - T T + Int T + T T - Int
Sum(Seq[V ])V ::= Var(String, String, . . . ) V (Any, . . . )C ::= B T op T ! C C && C C || C
And(C, . . . ) And(Seq[C ]) Or(C, . . . )op ::= <= < >= > === !==B ::= Bool(String, String, . . . ) B (Any, . . . )T - T

T * Int

Sum(V, . . . )Or(Seq[C ]) alldiff(Seq(T, . . . ))図 2. Scarab における制約の構文規則

2.1

Scala の概要

Scala は2 Martin Odersky により設計された比較的新しいプログラミング言語で，Twitter の分
散 DB フレームワークに用いられたことなどもあり，近年注目を集めている [17]. 言語上の特長としては，関数型言語とオブジェクト指向言語の融合，強力な型推論，型安全性，高階関数，不変コ
レクションなどが挙げられる．
処理系としては，JVM (Java Virtual Machine) へのコンパイラとインタラクティブな実行環境(REPL; Read Eval Print Loop) が用意されている．Java との親和性は高く，Java のクラス・ライ
ブラリをそのまま利用できる．
さらに Scala は，関数型言語およびオブジェクト指向言語としての高度な記述能力，リスト，マップ，集合等の豊富なコレクションフレームワーク，演算子の多重定義や柔軟な構文，オブジェクトのメソッドのインポート機能など，埋込みの ドメイン特化言語 (DSL; Domain-specific Language)を実装するために適した機能を数多く備えている [12]. 特に Scarab DSL ではケースクラス，暗黙変換，シングルトンオブジェクトおよびそのオブジェクトからのインポートなどの機能を利用しているが，これらの詳細については文献 [17] を参照されたい．

2.2

Scarab DSL

Scarab DSL は Scala 上の埋込み DSL (embedded DSL) として実装されている．CSP における
項 (x + y 等の数式) および制約 ((x > 0) ∨ (y > 0) 等の論理式) を Scala 中で表現するために，次のようなクラスを定義する: Term (項を表すクラス), Var (整数変数を表すクラス), Bool (ブール変数を表すクラス), Constraint (制約を表すクラス). これらのクラスは jp.kobe u.scarab.csp パッ
ケージに属している．
図 2 に Scarab DSL における制約の構文規則を示す．ここで T ，V ，C ，B は上述の Term，Var，
Constraint，Bool クラスを表す．また Int ，String ，Seq をそれぞれ Scala における整数 (Integer)，
文字列 (String)，列 (Sequence) クラスとする．Any は全てのクラスの親クラスとする．論理演算子は|| と Or が論理和，&& と And が論理積を表している．加えて比較演算子として<= (≤), <, >=(≥), >, === (=), !== (̸=) を用意している．
Scarab DSL における制約定義の例を Scala の REPL の実行例を通して説明する．なお以下の
REPL 実行例では，import jp.kobe u.scarab.csp. の実行を仮定していることに注意されたい．
整数変数を表すクラス Var は，変数名に加え文字列のリストを添字として指定可能である．また，すでにある Var オブジェクトに任意の添字を追加した新しい Var オブジェクトを作成できるように，apply メソッドを定義している．
scala> val x = Var("x")
x: jp.kobe_u.scarab.csp.Var = x2

http://www.scala-lang.org/

44

MAGE Vol.34, No.42 (2014.7)

scala> x(1,2)
res0: jp.kobe_u.scarab.csp.Var = x(1,2)// x.apply(1,2) と同じ

これらの整数変数を用いた制約 x ≤ 1 ∨ x1,2 ≤ 1 の記述例を以下に示す．

scala> x <= 1 || x(1,2) <= 1
res1: jp.kobe_u.scarab.csp.Or =Or(LeZero(Sum(-1+x)),LeZero(Sum(-1+x(1,2))))∑
ここで注意されたいのは Scarab では制約中の線形制約は定義されるとまず i ai xi − c ≤ 0 (但しai は非零の整数 c は整数値，x i は整数変数) の形に変換されるということである．線形制約のクラスは LeZero である．上記の例では x ≤ 1 ∨ x1,2 ≤ 1 は x − 1 ≤ 0 ∨ x1,2 − 1 ≤ 0 に変換される．
この他に Scarab では Scala の暗黙変換を利用してシンボル (’ で始まる記号) を整数変数として利用できるようになっており，次のように簡潔に制約を記述できる．
scala> ’y <= 0 || ’y(1,2) <= 0
res2: jp.kobe_u.scarab.csp.Or =Or(LeZero(Sum(+y)),LeZero(Sum(+y(1,2))))
最後に Scarab DSL を用いた CSP の定義例を以下に示す．

// CSP の生成// 整数変数 x ∈ {1, . . . , 3} の追加// 整数変数 y ∈ {1, . . . , 3} の追加// 制約 x + y ≤ 2 の追加

scala> val csp = CSP()
scala> csp.int(’x, 1, 3)
scala> csp.int(’y, 1, 3)
scala> csp.add(’x + ’y <= 2)

Scarab では CSP の解を計算するために CSP ソルバーのクラス Solver を用意している．Solver
は jp.kobe u.scarab.solver パッケージに属しており, CSP の解を計算する find メソッドを提供している．find は与えられた CSP を SAT に符号化し，SAT ソルバーを呼び出すことで解の計算を行う．
以上 Scarab DSL について説明を行った．Scarab プログラムはこの Scarab DSL と Scala の両方を用いて記述される．ループはもちろんのこと Scala の全ての機能を用いたプログラミングが可能であり，CSP を簡潔に記述することができる．

3

Scarab プログラム例

本節では Scala と Scarab DSL を用いたプログラム例を説明する．なお本節のプログラム例では次のインポート文の実行を仮定している．

import jp.kobe u.scarab.csp.
import jp.kobe u.scarab.solver.
import jp.kobe u.scarab.sapp.
ここで jp.kobe u.scarab.sapp は Scarab のアプリケーションのためのシングルトンオブジェク
トであり，CSP，CSP ソルバーそれぞれのデフォルトオブジェクトや，それらに対する int, add,
find 等のメソッドを提供している．これによりデフォルトオブジェクトに対する操作を簡潔に記述可能となる．

45

MAGE Vol.34, No.42 (2014.7)

1: val nodes = Seq(1,2,3,4,5)
2: val edges = Seq((1,2),(1,5),(2,3),(2,4),(3,4),(4,5))
3: var maxColor = 4
4:
5: for (i <- nodes)
6:
int(’x(i),1,maxColor)
7: for ((i,j) <- edges)8:
add(’x(i) !== ’x(j))
9:
10: if(find) println(solution)

1
5

2

4

3

図 3. グラフ彩色問題例の Scarab プログラムと計算された解

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:

val n = 15; val s =36
for (i <- 1 to n) {int(’x(i),0,s-i)int(’y(i),0,s-i)
}

7
14

15

6

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)))

13

9

11

12

4
2

8

5
10
3 1

if (find) println(solution)
図 4. SP (15, 36) の Scarab プログラムと計算された解

3.1

グラフ彩色問題一つ目の例はグラフ彩色問題 (GCP) である．ここで G = (V, E) をグラフとする．但し V は n個の頂点の集合であり，E は辺の集合であり，m は許容する最大の彩色数を表すものとする．GCPは許容される数の色を用いて，必ず隣接頂点が異なる色になるように彩色する問題である．GCP が与えられた時に素直な制約モデルは各頂点 i (1 ≤ i ≤ n) の色を表す整数変数 xi ∈ {1, . . . , m} を用いる方法である．次に全ての隣接する頂点の対 {i, j} ∈ E) に対して制約 xi ̸= xj を定義する．
図 3 の中で 1 行目と 2 行目は例として与えられた同じ図中のグラフにおける頂点と辺を定義している．3 行目は彩色数を 4 として定義している．以上によりグラフと彩色数の定義が完了したので，
次は制約モデルである．まず初めに 5，6 行目では上述した各頂点の色を表す整数変数を定義している．ここで jp.kobe u.scarab.sapp. のインポートにより，明示的に指定しない限りは，デフォ
ルトの CSP オブジェクト csp にこれらの整数変数が追加されることに注意されたい．7，8 行目は同様に隣接頂点の色が異なるという制約を各辺に対して追加している．10 行目では find によって解の計算を行い，解が存在する場合は標準出力に印字する．このように Scarab では整数変数と制約を非常に簡潔に定義することができ，また SAT 符号化や SAT 解法の部分についてはバックエンドで処理されるため，ユーザは専用の符号化プログラムを記述する事無く簡単に SAT 技術を利用することが可能となる．

3.2

正方形詰込み問題

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

46

MAGE Vol.34, No.42 (2014.7)

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:

val n: Int = 5
val pos = (0 until n)for (i <- pos; j <- pos)int(’x(i,j),1,n)for (i <- pos) {add(alldiff(pos.map(j => ’x(i,j))))add(alldiff(pos.map(j => ’x(j,i))))add(alldiff(pos.map(j => ’x(j,(i+j+n-1)%n))))add(alldiff(pos.map(j => ’x(j,(i-j+n-1)%n))))
}

2

3

5

1

4

5

1

4

2

3

4

2

3

5

1

3

5

1

4

2

1

4

2

3

5

if (find) println(solution)
図 5. P LS(5) の Scarab プログラムと計算された解である．最も素直なモデリングは整数変数 xi , yi ∈ {0, . . . , s − i} をそれぞれの正方形 i(1 ≤ i ≤ n)に (xi , yi ) が正方形 i の左下の座標を指すようにするものである．以下の制約は任意の二つの正方形 i と j (但し 1 ≤ i < j ≤ n) が重なることを禁止する．

(xi + i ≤ xj )(xj + j ≤ xi )(yi + i ≤ yj )(yj + j ≤ yi )

∨
∨
∨

(1)

図 4 に SP (15, 36) の時の Scarab プログラムを示す. ScarabDSL を用いることで簡潔に上記のモデルを表現できている．4，5 行目の int メソッドは整数変数をデフォルト CSP に定義している．ここで’x，’y は Scala におけるシンボルオブジェクトを表しており，前述のように Scala の暗黙変換
により整数変数オブジェクトへと変換される．9 から 12 行目の add メソッドは式 (1) の制約を定義している．14 行目の find メソッドは，定義された CSP を SAT へと符号化した後に解を計算，逆符号化している．逆符号化された解は solution によって返され, Scala の println メソッドにより出力される．

3.3

汎対角線ラテン方陣

もう一つの例は CSP ソルバー競技会 [11] で使用された汎対角線ラテン方陣 (Pandiagonal Latin
Square) である．汎対角線ラテン方陣 LS(n) は n 行 n 列の行列に 1 から n までの n 個の異なる整
数を，各整数が各行，各列，各汎対角線に 1 回だけ現れるように配置する問題である．いま LS(n)が与えられたとき，整数変数の n 行 n 列の行列 xi,j ∈ {1, . . . , n} (1 ≤ i, j ≤ n) を用いてモデリングを行う．各整数が 1 回だけ現れる制約は alldiﬀ 制約 [18] によって表す．この制約は制約プログラ
ミングの分野で最もよく知られているグローバル制約の一つであり，与えられた n 個の整数変数が互いに異なることを意味する [30].
図 5 は LS(5) に対する Scarab プログラムを表している. ScarabDSL は alldiﬀ を用いたモデリングを Scala の特長を用いて簡潔に表している．例えば 7 行目の alldiff(elems.map(j => ’x(i,j)))
は各行においてそれぞれの変数が異なることを表す制約 alldiﬀ (xi,1 , xi,2 , . . . , xi,n ) を表している．

4

Sat4j を用いた高度な解法

Scarab では Sat4j をデフォルトの SAT ソルバーとして採用している．Scarab と Sat4j は共に JVM
上で実行可能であり，

47

MAGE Vol.34, No.42 (2014.7)

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:

// CSP 定義
int(’x, 1, 3)
int(’y, 1, 3)
add(x === y)// x ∈ {1, 2, 3}// y ∈ {1, 2, 3}// 制約の定義 x = y// 4.1 インクリメンタル解法
find
add(x !== 3)
find// 充足可能: x = 3, y = 3// 制約の追加// 充足可能: x = 2, y = 2// 4.2 Assumption を用いた解法
find(y === 3)find(x === 1)// 充足不能// 充足可能: x = 1, y = 1// 4.3 コミットとロールバック
commitadd(x < y)findrollbackfind// コミットポイント生成// x < y が追加される// 充足不能// x < y の追加をロールバック// 充足可能: x = 2, y = 2

図 6. Sat4j を用いた高度な解法の例

Sat4j は Scarab から外部プロセスの起動なしに直接実行可能であり，このような SAT ソルバーとの融合およびこれによる高度な解法は他の SAT 型制約プログラミングツールにはない Scarab の特長になっている．本節では図 6 に示すプログラム例を用いて Sat4j に実装されている機能を利用した Scarab の解法について説明を行う．

4.1

インクリメンタル解法

図 6 の 6〜9 行目に記載されるように, Scarab では一度解を計算した後に制約の追加が可能である．7 行目の 1 回目の find メソッドでは定義された CSP 全体が SAT 符号化され，生成された節集
合が Sat4j へと追加される．SAT ソルバー Sat4j が求解を行う．9 行目の 2 回目の find メソッドでは 8 行目で追加された制約 x ̸= 3 のみが符号化され，節集合が Sat4j に追加される．そして Sat4jが再び求解を行う．
ここで 1 回目の find メソッドによって生成された学習節は 2 回目の呼び出し時にも保持されており，学習節の再利用による効果的な解探索を期待できる．但し，1 回目の CSP が充足不能の場合には制約の追加は許可されないので注意されたい．

4.2

仮説を用いた解法

Scarab では制約を引数に持つ find(assump: Constraint) メソッドを用いる仮説 (Assumption)に基づく CSP の解探索が可能である．但し，現状は仮説に指定する制約はブール変数上のリテラルの連言に符号化される必要があり，それ以外の制約が指定された場合には例外が発生する．それぞれのリテラルは Sat4j へと渡されこの仮説リテラル集合に基づく SAT の解探索が Sat4j で行われる．
図 6 の例では，12 行目で仮説 y = 3 のもとで CSP の求解が行われている．しかし，この仮説はこれまで追加された制約 (x = y) ∧ (x ̸= 3) と矛盾するので充足不能が返される．続いて仮説 x = 1のもとで CSP の求解が行われ，この場合には充足可能となる．
このように仮説で指定した制約は CSP に永続的に追加されるのではなく，求解中にのみ有効であり，また探索中に得られた学習節も保持される．後述するように，この仮説を用いた解法は最適解のデクリメンタル探索や二分法へと応用することができる．

48

MAGE Vol.34, No.42 (2014.7)

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:

1:
2:
3:
4:
5:
for (i <- 1 to n)add((’x(i)+i <= ’m)&&(’y(i)+i <= ’m)) 6:
7:8:
while (lb <= ub && find(’m <= ub)) {9:add(’m <= ub)
10:
ub = solution.intMap(’m) - 1
11:
}
12:
13:
while (findNext)
14:
println(solution)

while (lb < ub) {var size = (lb + ub) / 2
for (i <- 1 to n)add((’x(i)+i<=size)&&(’y(i)+i<=size))if (find) {ub = size ; commit} else {lb = size + 1 ; rollback}}

図 7. 仮説を用いたデクリメンタル探索

図 8. commit/rollback を用いた二分探索

val lb = n
var ub = sint(’m, lb, ub)

4.3

var lb = n
var ub = s
commit制約のコミットとロールバック

Scarab では以下のような制約のコミット (commit) とロールバック (rollback) メソッドを提供している．
• commit メソッドは現在の CSP の状態 (整数変数，ブール変数，制約の数) を記録する．現在の Scarab の実装では一つのコミットポイントを作成可能である．
• rollback メソッドは CSP を最後のコミットポイントの状態まで戻す．同時に Sat4j の状態
も reset メソッドにより初期化されるので次回の find メソッド呼び出し時には Sat4j へと節を追加し直す必要がある．
これら commit/rollback メソッドを実行することで，これまでに追加した制約の削除が可能となり，動的な制約の変更が必要なアプリケーションに対して，より柔軟な解探索を提供することができると考えられる．しかし，符号化の手続きは繰り返し行う必要があり，CSP が充足不能になった場合には学習節は再利用できないので注意が必要である．
図 6 の例では，16 行目でコミットポイントが生成され，17 行目で制約 x < y が追加されている．
しかし，この制約はこれまで追加された制約 (x = y) と矛盾するので充足不能が返される．次に 19
行目で rollback メソッドが呼ばれ CSP が 16 行目の状態まで戻される．すなわち制約 (x = y) が削除される．20 行目で再び求解が行われ，この場合には CSP は充足可能となる．

4.4

最適値の探索本節では上述の 3 つの機能を用いた応用として解の最適化を紹介する．例として，図 4 に示した
正方形詰込み問題 SP (n, s) について，制約を充足するような最小の正方形の枠の大きさを計算する．
図 7 は仮説を用いたデクリメンタル探索のプログラムを示している．このプログラムは図 4 のプ
ログラムの最下部に追加することで実行可能であり，プログラム中の Scala の整数変数 n と s は図4 で定義されているものである．
まずプログラム 3 行目の整数変数 m ∈ {lb, . . . , ub} は正方形の枠のサイズを表している．5，6 行目で定義される制約は全ての正方形がサイズ m の枠をはみ出ないことを保証する．8 行目では findメソッドが仮説 m ≤ ub とともに呼ばれている. もし解が存在するならば, 制約 m ≤ ub が追加さ
れ，ub が m の最も最近の値から 1 つ小さい値に更新される (10 行目)．13，14 行目では全ての最適解が列挙されている．findNext は最後に得られた解の否定をブロック節として加えることで別の解の探索を行うようになっている．

49

MAGE Vol.34, No.42 (2014.7)

表 1. 汎対角線ラテン方陣における性能評価 (CPU 時間: 秒)

3
4
5
6
7
UNSAT UNSAT SAT UNSAT SAT
alldiﬀ (naive)
0.164 0.153 0.183 0.398 0.210
alldiﬀ (optimized) 0.230 0.209 0.236 0.264 0.221
n

8
UNSAT
T.O.
0.212

9
UNSAT
T.O.
0.235

15
16
10
11
12
13
14
UNSAT SAT UNSAT SAT UNSAT UNSAT UNSAT
alldiﬀ (naive)
T.O. 0.347 T.O. T.O. T.O.
T.O.
T.O.
alldiﬀ (optimized) 0.370 0.332 0.981 0.545 9.792 389.917 458.187
n

図 8 は commit/rollback メソッドと制約の追加を用いた二分探索を示している．6 行目は現在の下限と上限のちょうど半分の値を計算している．7，8 行目は正方形の枠の大きさを制限する制約を追加している．9 行目では, find メソッドが呼ばれている．もし CSP が充足可能である場合, 上限が更新され現在の CSP がコミットされる (10 行目). もし充足不能である場合, 下限が 1 だけ増加
され最後のコミットポイントへと CSP がロールバックされる (12 行目).

5

性能評価

Scarab の基本性能を評価するために図 5 で示した汎対角線ラテン方陣を用いて計算機実験を行った．ここでは二つの alldiﬀ 制約の実装を用いた．一つめは naive 版で alldiﬀ 制約の定義に従い与∧えられた n 個の変数 x1 , . . . , xn の入力に対し， 1≤i<j≤n (xi ̸= xj ) なる制約を定義するものである．
∧∨n∧
二つめは optimized 版で，順列制約 ub
i=lb j=1 (xj = i) と鳩ノ巣原理の制約 ¬ (xi < lb + n − 1)∧and ¬ (xi > ub − n + 1) を naive 版に加えたものである．この鳩の巣原理の制約の効果は文献[22] で報告されている．なお naive 版は Scarab では 2 行で実装されており optimized 版でも 15行程度である．このように制約の実装を簡潔に記述でき，改良したものを実験できることは Scarab
で SAT 型システム開発を行う利点の一つである．
性能評価の制限時間は 1 時間で，全ての計算時間は Xeon 2.93GHz の CPU，JVM に対して 2GBのメモリを割当てた MacOS X 上で行っている．表 1 は P LS(n) (但し 3 ≤ n ≤ 16) に対する Scarabの計算時間 (CPU 時間，秒) を示している．optimized 版 alldiﬀ 制約を用いたものは n = 16 までを解くことに成功している．2009 年に開催された CSP ソルバー競技会では n ≤ 12 までを解いた
Sugar を除くと n > 8 の P LS(n) を 1800 秒以内にどの CSP ソルバーも解くことができなかったことから Scarab はこの問題において良い性能を示しているといえる．

6

おわりに

この論文では Scala 上に実装された SAT 型制約プログラミングシステム開発ツールである Scarab の説明を行った．正方形詰込み問題と汎対角線ラテン方陣の二つの例によって示されるように ScarabDSLと Scala の特長を利用することで SAT 型システム開発者は簡潔に問題のモデリングを行うことができる．また Sat4j の機能を用いることで, Scarab は次の機能を提供する: インクリメンタル探索; 仮説を用いた CSP の解探索; 制約のコミットとロールバック. これらの機能は Scarab において最適化
や解列挙などの高度な機能を実装するのに使うことができる．
Scarab の興味深い拡張の一つとして Sat4j の機能をさらに導入することがある. 例えば Sat4j は与えられた CNF 式が充足不能である時に Minimal Unsatisfiable Subformula (MUS) を計算する

50

MAGE Vol.34, No.42 (2014.7)ことが可能である. 加えて埋め込みの最適化メソッドおよび解列挙メソッド，また基数制約や擬似
ブール制約なども入力として扱うことが可能である．Scarab が持つ制約表現および SAT 符号化モジュールとこれら Sat4j の機能の組合せは SAT 技術の応用を広げることを期待できる．Scarab の情報とソースコードは以下から入手できる. http://kix.istc.kobe-u.ac.jp/~soh/scarab/.

参考文献[1] Ansótegui, C. and Manyà, F.: Mapping Problems with Finite-Domain Variables into Problems with
Boolean Variables, Proceedings of the 7th International Conference on Theory and Applications ofSatisfiability Testing (SAT 2004), LNCS 3542, 2004, pp. 1–15.
[2] 番原睦則, 田村直之: SAT によるシステム検証, 人工知能学会誌, Vol. 25, No. 1(2010).
[3] Biere, A., Heule, M., van Maaren, H., and Walsh, T.(eds.): Handbook of Satisfiability, Frontiers in
Artificial Intelligence and Applications (FAIA), Vol. 185, IOS Press, 2009.
[4] Gavanelli, M.: The Log-Support Encoding of CSP into SAT, Proceedings of the 13th International
Joint Conference on Principles and Practice of Constraint Programming (CP 2007), LNCS 4741,
2007, pp. 815–822.
[5] Gent, I. P. and Nightingale, P.: A New Encoding of Alldiﬀerent into SAT, Proceedings of the 3rdInternational Workshop on Modelling and Reformulating Constraint Satisfaction Problems, 2004.
[6] Gent, I. P.: Arc Consistency in SAT, Proceedings of the 15th European Conference on Artificial
Intelligence (ECAI 2002), 2002, pp. 121–125.
[7] Hebrard, E., O’Mahony, E., and O’Sullivan, B.: Constraint Programming and Combinatorial Optimisation in NumberJack, Proceedings of CPAIOR, 2010, pp. 181–185.
[8] 井上克巳, 田村直之: SAT ソルバーの基礎, 人工知能学会誌, Vol. 25, No. 1(2010).
[9] Iwama, K. and Miyazaki, S.: SAT-Variable Complexity of Hard Combinatorial Problems, Proceedingsof the IFIP 13th World Computer Congress, 1994, pp. 253–258.
[10] Le Berre, D. and Parrain, A.: The Sat4j library, release 2.2, Journal on Satisfiability, Boolean Modelingand Computation, Vol. 7, No. 2-3(2010), pp. 59–6.
[11] Lecoutre, C., Roussel, O., and van Dongen, M. R. C.: Promoting Robust Black-box Solvers ThroughCompetitions, Constraints, Vol. 15, No. 3(2010), pp. 317–326.
[12] Mernik, M., Heering, J., and Sloane, A. M.: When and how to develop domain-specific languages,
ACM Comput. Surv., Vol. 37, No. 4(2005), pp. 316–344.
[13] Metodi, A. and Codish, M.: Compiling finite domain constraints to SAT with BEE, TPLP, Vol. 12,
No. 4-5(2012), pp. 465–483.
[14] 鍋島英知: SAT によるプランニングとスケジューリング, 人工知能学会誌, Vol. 25, No. 1(2010).
[15] 鍋島英知, 宋剛秀: 高速 SAT ソルバーの原理, 人工知能学会誌, Vol. 25, No. 1(2010).
[16] 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳: パッキング配列問題の制約モデリングと SAT 符号化,
コンピュータソフトウェア, Vol. 31, No. 1(2013), pp. 116–130.
[17] Odersky, M., Spoon, L., and Venners, B.: Programming in Scala, Artima, Inc., second edition, 2010.
[18] Régin, J.-C.: A Filtering Algorithm for Constraints of Diﬀerence in CSPs, Proceedings of the 12th
National Conference on Artificial Intelligence (AAAI 1994), 1994, pp. 362–367.
[19] 宋剛秀, 番原睦則, 田村直之, Le Berre, D., Roussel, S.: Scala 上で実現された SAT 型制約プログラミ
ングシステムのための開発ツール Scarab について, 日本ソフトウェア科学会第 30 回大会講演論文集,
PPL2-5, 日本ソフトウェア科学会, 2013.
[20] Soh, T., Le Berre, D., Roussel, S., Banbara, M., and Tamura, N.: Incremental SAT-based Methodwith Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem, Proceedings of the 14th
European Conference on Logics in Artificial Intelligence, to appear, 2014.
[21] Soh, T., Tamura, N., and Banbara, M.: Scarab: A Rapid Prototyping Tool for SAT-Based Constraint
Programming Systems, SAT, 2013, pp. 429–436.
[22] 田島宏史: SAT 変換に基づく制約ソルバーの高速化に関する研究, 修士論文, 神戸大学大学院自然科学研
究科, 2006.

51

MAGE Vol.34, No.42 (2014.7)[23] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Constraints, Vol. 14, No. 2(2009), pp. 254–272.
[24] Tamura, N., Tanjo, T., and Banbara, M.: System Description of a SAT-based CSP Solver Sugar,
Proceedings of the 3rd International CSP Solver Competition, 2008, pp. 71–75.
[25] 田村直之, 丹生智也, 番原睦則: SAT 変換に基づく制約ソルバーとその性能評価, コンピュータソフト
ウェア, Vol. 27, No. 4(2010), pp. 183–196.
[26] 田村直之, 丹生智也, 番原睦則: 制約最適化問題と SAT 符号化, 人工知能学会誌, Vol. 25, No. 1(2010).
[27] 田村直之, 丹生智也, 番原睦則: Scala 上の制約プログラミング用ドメイン特化言語 Copris について, コ
ンピュータソフトウェア, Vol. 29, No. 4(2012), pp. 114–129.
[28] 丹生智也, 田村直之, 番原睦則: 位取り記数法に基づく整数有限領域上の制約充足問題のコンパクトかつ効率的な SAT 符号化, コンピュータソフトウェア, Vol. 30, No. 1(2013), pp. 211–230.
[29] Tseitin, G. S.: On the complexity of derivations in the propositional calculus, Studies in Mathematics
and Mathematical Logic Part II, (1968), pp. 115―–125.
[30] van Hoeve, W.-J. and Katrie, I.: Global Constraint, Handbook of Constraint Programming, Foundations of Artificial Intelligence, Elsevier, 2006, pp. 169–208.
[31] Walsh, T.: SAT v CSP, Proceedings of the 6th International Conference on Principles and Practiceof Constraint Programming (CP 2000), 2000, pp. 441–456.
[32] Zhou, N.-F.: The language features and architecture of B-Prolog, Theory and Practice of Logic Programming, Vol. 12, No. 1-2(2012), pp. 189–218.

52