日本ソフトウェア科学会第 30 回大会 (2013 年度) 講演論文集

Scala 上で実現された SAT 型制約プログラミングシス
テムのための開発ツール Scarab について
宋 剛秀 番原 睦則 田村 直之
Daniel Le Berre Stéphanie Roussel
Scarab は制約プログラミングのためのドメイン特化言語, SAT 符号化モジュール, SAT ソルバーへのインター
フェースから構成されており，SAT 型制約プログラミングシステム開発者を対象に，表現性，変更性，効率性を備えたワークベンチを提供することを目的としたツールである．Scarab は著者らが開発した Scala 上の制約プログラ
ミング用ドメイン特化言語である Copris と同様のツールである．しかし Scarab では，SAT ソルバー以外の部分
は，SAT 符号化の部分を含めてすべて Scala でコンパクトに記述されており変更が容易であるという特長を持つ．
また SAT ソルバーとして利用している Sat4j に対する API を使用することにより，インクリメンタル解法などのSAT 技術を用いた高度な解法が実現可能である点も特長の一つである．本論文では，Scarab の構成とプログラム例
を通してその機能と特長について説明を行う．

のための ドメイン特化言語 (DSL; Domain-specific

1 はじめにLanguage) である Scarab DSL, SAT 符号化モジュー

命題論理の充足可能性判定 (SAT; Boolean (orル，そしてバックエンドの SAT ソルバーへのインター

propositional) satisfiability (testing)) は人工知能やフェースから構成される．現在，Scarab では SAT 符

計算機科学の分野において重要である [3] [8]. この十数号化として順序符号化 [19] ，SAT ソルバーには Sat4j

年で SAT 問題を解くためのプログラムである SAT[10] を利用可能である．

ソルバー の性能は飛躍的に向上しており [15]，このScarab の設計方針は SAT 型システム開発者に表現ような性能向上は与えられた問題を SAT 問題に符号性，効率性，変更性，可搬性を備えたワークベンチを化し，SAT ソルバーを用いて解を求める SAT 型 シ

提供することである．

ステム の開発を促進してきた．例えば論理合成，プランニング，スケジューリング，ハードウェア・ソフ
トウェアの検証，制約充足問題などで SAT 型システ
ムが成功をおさめている [8] [2] [22] [14]．

表現性:

Scarab DSL と Scala の両方を用いて与えられた問題を記述することが可能である．
効率性:

Scarab は最適化された順序符号化法を用いているという点で効率的である [19]．順序符

本論分では Scala 上で実装された SAT 型制約プ

号化は 2008 年，2009 年に CSP ソルバー競技会

ログラミングシステムのための開発ツールである
Scarab†1 を提案する．Scarab は制約プログラミングのグローバル部門で優勝した Sugar [20] に採用さScarab: A Prototyping Tool for SAT-based Constraint
Programming Systems in Scala
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura,
神戸大学情報基盤センター, Information Science andTechnology Center, Kobe University.
Daniel Le Berre, Stéphanie Roussel, CRIL-CNRS,UMR 8188, Université d’Artois.
†1 http://kix.istc.kobe-u.ac.jp/~soh/scarab/

れている．
変更性:

Scarab では SAT 型システム開発者が自前の制約を定義し，変更・改良することが可能である．また Scarab のソースコードは全体で 500行ほどであり，Scarab 本体の変更も可能である．
可搬性:

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

CSP

SAT 符号化

オブジェクト

SAT

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

Sat4j

MAP

(DSL+Scala)

CSPの解Scarab DSL

逆符号化
CSP ソルバー API

図1

SAT
の解

SAT ソルバー API

Scarab の構成

図 1 に Scarab の構成図を示す．まず SAT 型シス

は Scala と制約プログラミングのための DSL であテム開発者が Scala と Scarab DSL を用いて記述しる Scarab DSL の両方を利用可能である．本節ではたプログラム (Scarab プログラム) によって CSP オ

Scala と Scarab DSL を説明した後，Scarab プログ

ブジェクトが生成される．次に Scarab プログラムにラムの二つの例について説明を行う.

よって CSP ソルバーが求解のために API を通して呼ばれた時に，CSP オブジェクトは SAT オブジェクトへと変換される．続いて CSP ソルバーから SAT ソ

2. 1 Scala の概要
Scala は†2 Martin Odersky により設計された比ルバー Sat4j が API を通して実行される．解が存在

較的新しいプログラミング言語で，Twitter の分散

すれば逆符号化を通して CSP の解が返される．

DB フレームワークに用いられたことなどもあり，近これまで SAT 型システムのための制約プログラミン

年注目を集めている [16]. 言語上の特長としては，関グ DSL はいくつか提案されている: Copris (in Scala)

数型言語とオブジェクト指向言語の融合，強力な型推[23], Numberjack (in Python) [7], Bee (in Prolog)

論，型安全性，高階関数，不変コレクションなどが挙[13], and B-Prolog (in Prolog) [28]. この中でも, 著げられる．

者らが開発した Copris は Scala 上の埋込み DSL を処理系としては，JVM (Java Virtual Machine) へ備えており Scarab と同様のツールである．Copris とのコンパイラとインタラクティブな実行環境 (REPL;

Scarab の違いとして，Scarab は 500 行で実装されてRead Eval Print Loop) が用意されている．Java といるなど，よりコンパクトで変更容易であることがの親和性は高く，Java のクラス・ライブラリをその挙げられる．また Scarab と SAT ソルバー Sat4j のまま利用できる．

親和性が高いことも Scarab の大きな特長である．第さらに Scala は，関数型言語およびオブジェクト

4 節で説明されるようにこの高い親和性により高度な指向言語としての高度な記述能力，リスト，マップ，解法が利用可能になる．

集合等の豊富なコレクションフレームワーク，演算子

以下では第 2 節で Scarab プログラムと二つの例をの多重定義や柔軟な構文，オブジェクトのメソッド説明する．次に SAT 符号化モジュールについて第 3のインポート機能など，埋込みの ドメイン特化言語

節で述べる．第 4 節は Sat4j を用いた高度な解法に(DSL; Domain-specific Language) を実装するためついて紹介し，第 5 節では汎対角線ラテン方陣を用に適した機能を数多く備えている [12]. 特に Scarab

いた性能評価を示す．

DSL ではケースクラス，暗黙変換，シングルトンオ
ブジェクトおよびそのオブジェクトからのインポート

2 Scarab プログラムなどの機能を利用しているが，これらの詳細について

Scarab を用いた SAT 型制約プログラミングシス

は文献 [16] を参照されたい．

テム開発の最も基本的な方法は Scarab プログラムを記述することである．Scarab プログラムの記述に†2 http://www.scala-lang.org/

T ::= V-T

T + Int

T +T

V ::= Var(String, String, . . . )C ::= BT op T! C

And(C, . . . )op ::= <=<>=T - Int===

T * Int

Sum(V, . . . )Sum(Seq[V ])V (Any, . . . )C && C

And(Seq[C ])>T -T

C || C
Or(C, . . . )Or(Seq[C ])alldiff(Seq(T, . . . ))!==B ::= Bool(String, String, . . . )B (Any, . . . )図2

Scarab における制約の構文規則

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 は全てのクラスの親クラスとする．論理演算子は|| と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))))

Or が論理和，&& と And が論理積を表している．加

最後に Scarab DSL を用いた CSP の定義例を以下にえて比較演算子として<= (≤), <, >= (≥), >, === (=),

示す．

!== (̸=) を用意している．
Scarab DSL に お け る 制 約 定 義 の 例 を Scalaの REPL の 実 行 例 を 通 し て 説 明 す る (importjp.kobe u.scarab.csp. の実行を仮定している)．
整数変数を表すクラス Var は，変数名に加え文字列のリストを添字として指定可能である．また，すでにある Var オブジェクトに任意の添字を追加した新しい Var オブジェクトを作成できるように，apply メ
ソッドを定義している．
scala> val x = Var("x")
x: jp.kobe_u.scarab.csp.Var = x
scala> x(1,2)// x.apply(1,2) と同じ
res0: jp.kobe_u.scarab.csp.Var = x(1,2)

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

// CSP の生成
scala> val csp = CSP()// 整数変数 x, y ∈ {1, . . . , 3} の追加
scala> csp.int(’x, 1, 3)
scala> csp.int(’y, 1, 3)// 制約 x + y ≤ 2 の追加
scala> csp.add(’x + ’y <= 2)

Scarab では CSP の解を計算するために CSP ソ
ルバーのクラス Solver を用意している．Solver は

jp.kobe u.scarab.solver パッケージに属しており,
CSP の解を計算する find メソッドを提供している．
find は与えられた CSP を SAT に符号化し，SAT ソ
ルバーを呼び出すことで解の計算を行う．Scarab における SAT 符号化については第 3 節で説明を行う.

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

val n = 15; val s =36

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

for (i <- 1 to n) {int(’x(i),0,s-i)int(’y(i),0,s-i)}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)))
if (find) println(solution)
図3

SP (15, 36) の Scarab プログラム

val n: Int = 5
val elems = (0 until n)for (i <- elems; j <- elems)int(’x(i,j),1,n)for (i <- elems) {add(alldiff(elems.map(j => ’x(i,j))))add(alldiff(elems.map(j => ’x(j,i))))add(alldiff(elems.map(j => ’x(j,(i+j+n-1)%n))))add(alldiff(elems.map(j => ’x(j,(i-j+n-1)%n))))}if (find) println(solution)
図4

LS(5) の Scarab プログラム

2. 3 Scarab プログラム例
本節では Scala と Scarab DSL を用いたプログラ

数変数をデフォルト CSP に定義している．ここでム例を説明する．なお本節のプログラム例では次のイ’x，’y は Scala におけるシンボルオブジェクトを表

ンポート文の実行を仮定している．

しており，前述のように Scala の暗黙変換により整数

import jp.kobe u.scarab.csp.
import jp.kobe u.scarab.solver.
import jp.kobe u.scarab.sapp.

変数オブジェクトへと変換される．9 から 12 行目のadd メソッドは式 (1) の制約を定義している．14 行

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

目の find メソッドは，定義された CSP を SAT へと符号化した後に解を計算，逆符号化している．逆符号化された解は solution によって返され, Scala のprintln メソッドにより出力される．
2. 3. 2 汎対角線ラテン方陣
もう一つの例は CSP ソルバー競技会 [11] で使用さジェクトに対する操作を簡潔に記述可能となる．

れた汎対角線ラテン方陣 (Pandiagonal Latin Square)

2. 3. 1 正方形詰込み問題
一つめの例は正方形詰込み問題を解くプログラムである．正方形詰込み問題 SP (n, s) は一辺の長さ 1 から n まで 1 ずつ増加する正方形の集合を一辺の長さ sの正方形の枠内に重なりなく配置する問題である．最も素直なモデリングは整数変数 xi , yi ∈ {0, . . . , s − i}をそれぞれの正方形 i(1 ≤ i ≤ n) に (xi , yi ) が
正方形 i の左下の座標を指すようにするものである．以下の制約は任意の二つの正方形 i と j (但し∨(yi + i ≤ yj )∨列に 1 から n までの n 個の異なる整数を，各整数が各行，各列，各汎対角線に 1 回だけ現れるように配置する問題である．いま LS(n) が与えられたとき，整数変数の n 行 n 列の行列 xi,j ∈ {1, . . . , n} (1 ≤ i, j ≤ n)を用いてモデリングを行う．各整数が 1 回だけ現れる
制約は alldiﬀ 制約 [17] によって表す．この制約は制約プログラミングの分野で最もよく知られているグ
ローバル制約の一つであり，与えられた n 個の整数

1 ≤ i < j ≤ n) が重なることを禁止する．
(xi + i ≤ xj )∨(xj + j ≤ xi )である．汎対角線ラテン方陣 LS(n) は n 行 n 列の行

変数が互いに異なることを意味する [26].
図 4 は LS(5) に対する Scarab プログラムを表し(1)ている. Scarab DSL は alldiﬀ を用いたモデリング(yj + j ≤ yi )図 3 に SP (15, 36) の時の Scarab プログラムを示

を Scala の特長を用いて簡潔に表している．例えばす. Scarab DSL を用いることで簡潔に上記のモデ行においてそれぞれの変数が異なることを表す制約

ルを表現できている．4，5 行目の int メソッドは整

alldiﬀ (xi,1 , xi,2 , . . . , xi,n ) を表している．

7 行目の alldiff(elems.map(j => ’x(i,j))) は各 x1 ≤ ⌊c/a1 ⌋¬ (x1 ≤(⌈c/a1 ⌉ − 1))ub(x )
n

∑
n
 ∧1
∑
(x1 ≤ b − 1) ∨ai xi ≤ c − a1 b
ai xi ≤ c =
i=2
b=lb(x1 )

i=1

(
)

ub(x1 )
n

∧
∑



¬(x1 ≤ b) ∨ai xi ≤ c − a1 b(n = 1, a1 > 0)(2a)(n = 1, a1 < 0)(2b)(n ≥ 2, a1 > 0)(2c)(n ≥ 2, a1 < 0)

(2d)

i=2

b=lb(x1 )図5

順序符号化における変換

3 Scarab における SAT 符号化
Scarab では与えられた CSP を，前処理により一旦
CSP の CNF 式に変換している．CSP の CNF 式におけるリテラルは，ブール変数，ブール変数の否定，∑ni=1 ai xi ≤ c の形の線形制約のいずれかである．ここで ai は非零の整数, c は整数値, そして xi は整数変数を表す. なお変換は Tseitin 変換 [25] [21] を用いて新しいブール変数を導入する方法で行っている．以下では Scarab で採用している SAT 符号化である順
序符号化とその実装について概要を説明する．

3. 1 順序符号化
順序符号化法 [19] ではブール変数 p(x ≤ c) がそれ
ぞれの整数変数 x と整数値 c ∈ {lb(x)−1, . . . , ub(x)}に対して導入される．ここで lb(x) と ub(x) はそれ

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

def encodeLe(axs: Seq[(Int,Var)], c: Int):
Seq[Seq[Literal]] = axs match {case Seq((a,x)) =>if (a > 0) Seq(Seq(le(x, floorDiv(c, a))))else Seq(Seq(le(x, ceilDiv(c, a)-1).neg))case Seq((a,x), axs1 @ _*) => {if (a > 0) {for {b <- lb(x) to ub(x)clause <- encodeLe(axs1, c-a*b)} yield le(x, b-1) +: clause} else {for {b <- lb(x) to ub(x)clause <- encodeLe(axs1, c-a*b)} yield le(x, b).neg +: clause
}
}
}
図6

順序符号化の実装

ぞれ x の下限値と上限値である．さらに以下の整数
変数における値の順序関係を表す制約が導入される．

∧

目はそれぞれ変換式 (2a) と (2b) を表している．9から 12 行目は変換式 (2c) を表している．11 行目でub(x)−1は {(a2 , x2 ), . . . , (an , xn )} と c − a1 b を入力として(¬p(x ≤ c − 1) ∨ p(x ≤ c))encodeLe を再帰的に呼び出している．14 から 17 行

c=lb(x)+1

順序符号化法では線形制約∑ni=1 ai xi≤ c を符

号 化 す る た め に 図 5 に 示 す 変 換 式 を 用 い る.

この変換を再帰的に適用し，変換式 (2a) と (2b) のx1 ≤ ⌊c/a1 ⌋ と x1 ≤ ⌈c/a1 ⌉ − 1 をそれぞれブール変数 p(x1 ≤ ⌊c/a1 ⌋) と p(x1 ≤ ⌈c/a1 ⌉ − 1) に変換する
ことで最終的に線形制約はブール変数上の連言標準形式へと変換される．

3. 2 順序符号化の実装
図 6 は図 5 の変換を実装したプログラムを
示 し て い る ．1 行 目 は 二 つ の 入 力 を 表 し て お り，{(a1 , x1 ), . . . , (an , xn )} と整数値 c である．5，6 行

目は同様に変換式 (2d) を表している．
例 と し て 正 方 形 詰 込 み 問 題 SP (2, 6) の 制 約 の一 部 で あ る 制 約 x1 + 1 ≤ x2 を 考 え る ．こ こ でx1 ∈ {0, . . . , 5} と x2 ∈ {0, . . . , 4} とする．まず初めに x1 + 1 ≤ x2 は線形制約 x1 − x2 ≤ −1 に変形される. 図 6 の encodeLe を入力 {(1, x1 ), (−1, x2 )} と−1 に入力として呼ぶことにより, 以下の順序符号化された CNF 式が得られる:¬p(x2 ≤ 0) ∧(p(x1 ≤ 0) ∨ ¬p(x2 ≤ 1)) ∧(p(x1 ≤ 1) ∨ ¬p(x2 ≤ 2)) ∧(p(x1 ≤ 2) ∨ ¬p(x2 ≤ 3)) ∧p(x1 ≤ 3) ∧ p(x1 ≤ 4)

体が SAT 符号化され，生成された節集合が Sat4j へ
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) // x ∈ {1, 2, 3}
int(’y, 1, 3) // y ∈ {1, 2, 3}
add(x === y) // 制約の定義 x = y// 4.1 インクリメンタル解法
find// 充足可能: x = 3, y = 3
add(x !== 3) // 制約の追加
find// 充足可能: x = 2, y = 2と追加される．SAT ソルバー Sat4j が求解を行う．9
行目の 2 回目の find メソッドでは 8 行目で追加された制約 x ̸= 3 のみが符号化され，節集合が Sat4j に追加される．そして Sat4j が再び求解を行う．
ここで 1 回目の find メソッドによって生成された学習節は 2 回目の呼び出し時にも保持されており，学習節の再利用による効果的な解探索を期待できる．

// 4.2 Assumption を用いた解法
find(y === 3) // 充足不能
find(x === 1) // 充足可能: x = 1, y = 1// 4.3 コミットとロールバック
commit// コミットポイント生成
add(x < y)// x < y が追加される
find// 充足不能rollback// x < y の追加をロールバック
find// 充足可能: x = 2, y = 2
図7

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

但し，1 回目の CSP が充足不能の場合には制約の追加は許可されないので注意されたい．

4. 2 仮説を用いた解法
Scarab で は 制 約 を 引 数 に 持 つ find(assump:
Constraint) メソッドを用いる仮説 (Assumption)に基づく CSP の解探索が可能である．但し，現状は仮説に指定する制約はブール変数上のリテラルの連言に符号化される必要があり，それ以外の制約が指定

実際の Scarab 中の encodeLe の実装も 25 行以内された場合には例外が発生する．それぞれのリテラルとコンパクトであり，SAT 型システム開発者が SAT

は Sat4j へと渡されこの仮説リテラル集合に基づく符号化を変更し易いようになっている．また Scarab

SAT の解探索が Sat4j で行われる．

の符号化インターフェースを用いてこれまで提案さ

図 7 の例では，12 行目で仮説 y = 3 のもとで CSP

れてきた他の SAT 符号化を実装することも可能であの求解が行われている．しかし，この仮説はこれまで

る [9] [27] [6] [5] [1] [4] [24]. この際には整数変数と制約の追加された制約 (x = y) ∧ (x ̸= 3) と矛盾するので充SAT 符号化および逆符号化メソッドの実装が必要に足不能が返される．続いて仮説 x = 1 のもとで CSPなる．

の求解が行われ，この場合には充足可能となる．
このように仮説で指定した制約は CSP に永続的に4 Sat4j を用いた高度な解法追加されるのではなく，求解中にのみ有効であり，まScarab では Sat4j をデフォルトの SAT ソルバーとた探索中に得られた学習節も保持される．後述するよ

して採用している．Scarab と Sat4j は共に JVM 上

うに，この仮説を用いた解法は最適解のデクリメンタ

で実行可能であり，

ル探索や二分法へと応用することができる．

Sat4j は Scarab から外部プロセスの起動なしに直接実行可能であり，このような SAT ソルバーとの融4. 3 制約のコミットとロールバック

合およびこれによる高度な解法は他の SAT 型制約

Scarab では以下のような制約のコミット (commit)

プログラミングツールにはない Scarab の特長になっとロールバック (rollback) メソッドを提供している．

ている．本節では図 7 に示すプログラム例を用いて• commit メソッドは現在の CSP の状態 (整数変Sat4j に実装されている機能を利用した Scarab の解数，ブール変数，制約の数) を記録する．現在の法について説明を行う．

Scarab の実装では一つのコミットポイントを作成可能である．

4. 1 インクリメンタル解法
図 7 の 6〜9 行目に記載されるように, Scarab では
一度解を計算した後に制約の追加が可能である．7 行
目の 1 回目の find メソッドでは定義された CSP 全• rollback メソッドは CSP を最後のコミットポ
イントの状態まで戻す．同時に Sat4j の状態も

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

val lb = n
var ub = sint(’m, lb, ub)for (i <- 1 to n)add((’x(i)+i <= ’m) && (’y(i)+i <= ’m))while (lb <= ub && find(’m <= ub)) {add(’m <= ub)
ub = solution.intMap(’m) - 1}
while (find)println(solution)
図8

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

reset メソッドにより初期化されるので次回の

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

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

図9commit/rollback メソッドを用いた二分探索

find メソッド呼び出し時には Sat4j へと節を追加し直す必要がある．

義される制約は全ての正方形がサイズ m の枠をはみ

これら commit/rollback メソッドを実行すること

出ないことを保証する．8 行目では find メソッドがで，これまでに追加した制約の削除が可能となり，動仮説 m ≤ ub とともに呼ばれている. もし解が存在的な制約の変更が必要なアプリケーションに対して，するならば, 制約 m ≤ ub が追加され，ub が m のより柔軟な解探索を提供することができると考えら最も最近の値から 1 つ小さい値に更新される (10 行

れる．しかし，符号化の手続きは繰り返し行う必要が目)．13，14 行目では全ての最適解が列挙されている．

あり，CSP が充足不能になった場合には学習節は再Scarab では, find メソッドが同じ CSP に対して呼利用できないので注意が必要である．

ばれると 2 回目からは最後に得られた解の否定をブ

図 7 の例では，16 行目でコミットポイントが生成され，17 行目で制約 x < y が追加されている．しロック節として加えることで別の解の探索を行うようになっている．

かし，この制約はこれまで追加された制約 (x = y)

図 9 は commit/rollback メソッドと制約の追加をと矛盾するので充足不能が返される．次に 19 行目で用いた二分探索を示している．6 行目は現在の下限とrollback メソッドが呼ばれ CSP が 16 行目の状態

上限のちょうど半分の値を計算している．7，8 行目まで戻される．すなわち制約 (x = y) が削除される．

は正方形の枠の大きさを制限する制約を追加してい20 行目で再び求解が行われ，この場合には CSP は充る．9 行目では, find メソッドが呼ばれている．もし

足可能となる．

CSP が充足可能である場合, 上限が更新され現在のCSP がコミットされる (10，11 行目). もし充足不能

4. 4 最適値の探索である場合, 下限が 1 だけ増加され最後のコミットポ

本節では上述の 3 つの機能を用いた応用として解イントへと CSP がロールバックされる.

の最適化を紹介する．例として，図 3 に示した正方
形詰込み問題 SP (n, s) について，制約を充足するよ

5 汎対角線ラテン方陣を用いた性能評価

うな最小の正方形の枠の大きさを計算する．

Scarab の基本性能を評価するために図 4 で示した

図 8 は仮説を用いたデクリメンタル探索のプログ

汎対角線ラテン方陣を用いて計算機実験を行った．こラムを示している．このプログラムは図 3 のプログ

こでは二つの alldiﬀ 制約の実装を用いた．一つめはラムの最下部に追加することで実行可能であり，プロ

naive 版で alldiﬀ 制約の定義に従い与えられた n 個∧の変数 x1 , . . . , xn の入力に対し， 1≤i<j≤n (xi ̸= xj )グラム中の Scala の整数変数 n と s は図 3 で定義されているものである．
まずプログラム 3 行目の整数変数 m ∈ {lb, . . . , ub}
は正方形の枠のサイズを表している．5，6 行目で定なる制約を定義するものである．二つめは optimized∧∨n
版で，順列制約 ub
i=lb
j=1 (xj = i) と鳩ノ巣原理の∧∧制約 ¬ (xi < lb + n − 1) and ¬ (xi > ub − n + 1)

表1

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

nalldiﬀ (naive)
alldiﬀ (optimized)nalldiﬀ (naive)
alldiﬀ (optimized)

3
UNSAT
0.164
0.230

4
UNSAT
0.153
0.209

5
SAT
0.183
0.236

6
UNSAT
0.398
0.264

7
SAT
0.210
0.221

8
UNSAT
T.O.
0.212

9
UNSAT
T.O.
0.235

10
UNSAT
T.O.
0.370

11
SAT
0.347
0.332

12
UNSAT
T.O.
0.981

13
SAT
T.O.
0.545

14
UNSAT
T.O.
9.792

15
UNSAT
T.O.
389.917

16
UNSAT
T.O.
458.187

を naive 版に加えたものである．この鳩の巣原理のさらに導入することがある. 例えば Sat4j は与えられ制約の効果は文献 [18] で報告されている．なお naive

た CNF 式が充足不能である時に Minimal Unsatisfi-

版は Scarab では 2 行で実装されており optimized

able Subformula (MUS) を計算することが可能であ版でも 15 行程度である．このように制約の実装をる. 加えて埋め込みの最適化メソッドおよび解列挙メ

簡潔に記述でき，改良したものを実験できることは

ソッド，また基数制約や擬似ブール制約なども入力とScarab で SAT 型システム開発を行う利点の一つでして扱うことが可能である．Scarab が持つ制約表現おある．

よび SAT 符号化モジュールとこれら Sat4j の機能の変換制限時間は 1 時間で，全ての計算時間は Xeon

組合せは SAT 技術の応用を広げることを期待できる．

2.93GHz の CPU，JVM に対して 2GB のメモリを割

Scarab の情報とソースコードは以下から入手できる.

当てた MacOS X 上で行っている．参考として 2009http://kix.istc.kobe-u.ac.jp/~soh/scarab/.

年に開催された CSP ソルバー競技会では n ≤ 12 までを解いた Sugar を除くと n > 8 の LS(n) をどの

参 考 文 献CSP ソルバーも解くことができなかった．

[ 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 Applicationsof Satisfiability Testing (SAT 2004), LNCS 3542,
2004.
[ 2 ] 番原睦則, 田村直之: SAT によるシステム検証, 人
工知能学会誌, Vol. 25, No. 1(2010).
[ 3 ] Biere, A., Heule, M., van Maaren, H., andWalsh, 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,

表 1 は LS(n) (但し 3 ≤ n ≤ 16) に対する Scarabの計算時間 (CPU 時間，秒) を示している．optimized
版 alldiﬀ 制約を用いたものは$n=16$までを解くことに成功している．

6 おわりにこの論文では Scala 上に実装された SAT 型制約プ
ログラミングシステム開発ツールである Scarab の説明を行った．正方形詰込み問題と汎対角線ラテン方
陣の二つの例によって示されるように Scarab DSL とScala の特長を利用することで SAT 型システム開発
者は簡潔に問題のモデリングを行うことができる．
また Sat4j の機能を用いることで, Scarab は次の機能を提供する: インクリメンタル探索; 仮説を用いた

CSP の解探索; 制約のコミットとロールバック. これ
らの機能は Scarab において最適化や解列挙などの高度な機能を実装するのに使うことができる．

Scarab の興味深い拡張の一つとして Sat4j の機能を

2010, pp. 181–185.
[ 8 ] 井上克巳, 田村直之: SAT ソルバーの基礎, 人工知能学会誌, Vol. 25, No. 1(2010).
[ 9 ] Iwama, K. and Miyazaki, S.: SAT-Variable
Complexity of Hard Combinatorial Problems,Proceedings of the IFIP 13th World Computer
Congress, 1994, pp. 253–258.
[10] Le Berre, D. and Parrain, A.: The Sat4j library,release 2.2, JSAT, 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, Theory andPractice of Logic Programming, Vol. 12, No. 45(2012), pp. 465–483.
[14] 鍋島英知: SAT によるプランニングとスケジューリ
ング, 人工知能学会誌, Vol. 25, No. 1(2010).
[15] 鍋島英知, 宋剛秀: 高速 SAT ソルバーの原理, 人工知能学会誌, Vol. 25, No. 1(2010).
[16] Odersky, M., Spoon, L., and Venners, B.: Programming in Scala, Artima, Inc., second edition,
2010.
[17] 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.
[18] 田島宏史: SAT 変換に基づく制約ソルバーの高速化に関する研究, 修士論文, 神戸大学大学院自然科学研究科, 2006.

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