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

Scala 上で実現された SAT 型制約プログラミングシス
テムのための開発ツール
宋 剛秀

番原 睦則

田村 直之

命題論理の充足可能性判定 (SAT) 問題を解くプログラムである SAT ソルバーが 2000 年以降大きく進歩しており，活発に開発と研究が行われている．このような背景から，様々な分野で SAT ソルバーを利用した SAT 型システム
が成功をおさめるようになった．通常 SAT 型システムには，与えられた問題を SAT 問題へと符号化する専用のプ
ログラムが必要になるが，この開発コストのために制約モデルや符号化方法など問題を解くうえで重要な役割を担う部分に注力できないという問題があった．本論文では SAT 型システムのための開発ツールである Scarab を提案する．Scarab は制約プログラミングのためのドメイン特化言語, SAT 符号化モジュール, SAT ソルバーへのインター
フェースから構成されており，SAT 型制約プログラミングシステム開発者を対象に，表現性，変更容易性，効率性を備えたワークベンチを提供することを目的としたツールである．Scarab はオブジェクト指向言語と関数型言語が融合された Scala 言語上にコンパクトに実装されている．バックエンドの SAT ソルバーに Java で実装された
Sat4j を用いることにより，インクリメンタル解法等の高度な解法を容易に実現できる点も特長の一つである．

て解くことができる SAT 型制約プログラミングシ

1 はじめにステムが開発されてきた [31] [34] [12] [20] [40]．例えば命題論理の充足可能性判定 (SAT; propositional

Sugar [31] は専用の制約言語で制約充足問題 (CSP;

satisfiability) 問題は計算理論において中心的であり，constraint satisfaction problem) を記述し，順序符

また人工知能や計算機科学の分野においても重要な号化 [30] によって SAT 問題へと符号化した後に SAT問題である [4] [13]. 2000 年以降 SAT 問題を解くためソルバーによって解を求める SAT 型制約プログラミのプログラムである SAT ソルバーの性能が飛躍的に

ングシステムである．2008 年と 2009 年に CSP ソル

向上しており [22]，このような性能向上は与えられた

バー競技会 [18] のグローバル制約部門で優勝し，また問題を SAT 問題に符号化し，SAT ソルバーを用いて近年では 2013 年にパッキング配列の最良解を更新す解を求める SAT 型システムの開発を促進してきた．

るのに用いられた [23]．

これまで論理合成，プランニング，スケジューリング，

このように Sugar をはじめとする SAT 型制約プロ

ハードウェア・ソフトウェアの検証などで SAT 型シ

グラミングシステムは高い求解性能を実現しつつある．

ステムが成功をおさめている [13] [3] [33] [21]．SAT 型

しかし一方で高度な SAT 型解法を容易に実現できるシステムは効果的な方法であるが，与えられた問題にような機能性についてはあまり注目がされていない．

対して提案した解法を毎回はじめから実装するのは

例えば，近年 Counterexample Guided Abstraction

効率が悪い．そこで制約充足問題 (CSP; constraint

Refinement (CEGAR) [5] のモデル検査以外への応

satisfaction problem) などの汎用的に問題を記述し用や，SAT ソルバーに SAT 節以外の制約を組込む，Prototyping Tool for SAT-based Constraint Programming Systems in Scala
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura,
神戸大学情報基盤センター, Information Science andTechnology Center, Kobe University.

組込み制約を用いた SAT 型解法が提案されている[15] [16] [8] [6] [28]．Sugar は専用の記述言語を用いることでユーザにとって理解し易い制約表現を可能にしているが，一方でループなどの汎用プログラミング

CSP

SAT 符号化

オブジェクト

SAT

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

Sat4j

MAP

(DSL+Scala)

CSPの解Scarab DSL

SAT
の解

逆符号化
CSP ソルバー API
図1

SAT ソルバー API

Scarab の構成

言語で提供されている制御構造を扱うことができず構成される．SAT 符号化には Sugar に採用されてい

CEGAR を直接記述できない．また SAT ソルバーとる順序符号化 [30] の他に組込み制約を用いた符号化の連携はファイルを介して外部プロセスを起動するこを利用可能である．また Scarab の大きな特長の一つとによって行なうなど SAT ソルバーをブラックボッ

は SAT ソルバー Sat4j [17] との密な連携である．共クスとして扱っている．これはいろいろな種類の SATに Java 仮想マシン (JVM) 上で動作し，Scarab からソルバーをコストをかけずに切り替えることが可能

API を通じて Sat4j の低レベル機能を自由に利用すであり，利点にもなるが SAT ソルバー内部の低レベることができる．また外部プロセスによる起動を許容

ル機能の利用と拡張には対応することが難しくなる．

すれば Sat4j 以外の SAT ソルバーも利用可能である．

上記のような機能性の議論に加えて，使い易い SAT

これらの外部 SAT ソルバー用の API も備えており，

型制約プログラミングシステムには与えられた問題

連言標準形で表される命題論理式 (CNF 式) が記述を簡単に記述できる表現性も重要である．Scala はされたファイルを入力とする SAT ソルバーを Scarab

Martin Odersky により設計された比較的新しいプロから利用することができる．

グラミング言語である [25]. 特長として関数型言語

Scarab の設計方針は SAT 型システム開発者に表現とオブジェクト指向言語の融合とドメイン特化言語性，効率性，変更性，可搬性を備え，SAT 符号化と(DSL; Domain-specific Language) を実装するため

SAT ソルバーをグラスボックス化したワークベンチに適した機能を数多く備えていることが挙げられる．

を提供することである．

また 2006 年の ACM Symposium on Programming

Languages and Systems (POPL) の Martin Odersky の招待講演において Scala のアプリケーションと表現性:

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

Scarab は最適化された順序符号化法をして制約プログラミングが示唆されており [24]，制約標準で用いているという点で効率的である [30]．

記述のためのドメイン特化言語を構築するのに適し

順序符号化は 2008 年，2009 年に CSP ソルバー

た言語の一つであると考えられる．

競技会のグローバル部門で優勝した Sugar [31] に

本論文では高度な SAT 解法を実現するためのワー
クベンチとして，Scala 上で実装された SAT 型制約プ
ログラミングシステム Scarab†1 を提案する．Scarab

採用されている．
変更性:

Scarab では SAT 型システム開発者が自前の制約を定義し，変更・改良することが可能では制約プログラミングのためのドメイン特化言語であある．また Scarab のソースコードは全体で 1000

る Scarab DSL, SAT 符号化モジュール，そしてバッ

行ほどであり，Scarab 本体の変更も可能である．

クエンドの SAT ソルバーへのインターフェースから

特に順序符号化の中心部分の実装は 20 行ほどで行われている．

†1 http://kix.istc.kobe-u.ac.jp/~soh/scarab/

可搬性:

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

DSL である Scarab DSL の両方を利用可能である．

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

本節では Scala と Scarab DSL を説明した後，二つテム開発者が Scala と Scarab DSL を用いて記述しの問題記述例を通して Scarab の基本的機能の説明をたプログラム (Scarab プログラム) によって CSP オ

行う.

ブジェクトが生成される．次に Scarab プログラムによって CSP ソルバーが求解のために API を通して呼ばれた時に，CSP オブジェクトは SAT オブジェクト

2. 1 Scala の概要
Scala は†2 Martin Odersky により設計された比へと変換される．続いて CSP ソルバーから SAT ソ

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

ルバー Sat4j が API を通して実行される．解が存在

DB フレームワークに用いられたことなどもあり，近すれば逆符号化を通して CSP の解が返される．

年注目を集めている [25]. 言語上の特長としては，関汎用プログラミング言語を制約記述に用いる SAT

数型言語とオブジェクト指向言語の融合，強力な型推型制約プログラミングシステムの従来研究として論，型安全性，高階関数，不変コレクションなどが挙Copris (in Scala) [34], Numberjack (in Python) [12],げられる．

Bee (in Prolog) [20], B-Prolog (in Prolog) [40] が挙処理系としては，JVM (Java Virtual Machine) へげられる．この中でも, 著者らが開発した Copris はのコンパイラとインタラクティブな実行環境 (REPL;

Scala 上の埋込み DSL を備えている点で Scarab と同

Read Eval Print Loop) が用意されている．Java と様のツールである．Copris では Sugar を SAT 符号化の親和性は高く，Java のクラス・ライブラリをそのモジュールとして用いており，SAT ソルバーを外部プ

まま利用できる．

ロセスとして起動するなど SAT ソルバーとの連携はさらに Scala は，関数型言語およびオブジェクト

疎に行われる．一方，Scarab は，SAT 符号化，SAT

指向言語としての高度な記述能力，リスト，マップ，

ソルバーのグラスボックス化を設計方針としており，集合等の豊富なコレクションフレームワーク，演算子

SAT 符号化モジュールを含めて Scala 上で 1000 行程の多重定義や柔軟な構文，オブジェクトのメソッド

度で実装されている．これによりコードはコンパクトのインポート機能など，埋込みの ドメイン特化言語

で変更容易であり，新しいアイデアを実験し易い．ま(DSL; Domain-specific Language) を実装するためた SAT ソルバーとの密な連携によりインクリメンタに適した機能を数多く備えている [19]. 特に Scarab

ル解法や組込み制約など SAT ソルバーの低レベル機

DSL ではケースクラス，暗黙変換，シングルトンオ能の利用ができる点，それらを Scala 上で拡張できるブジェクトおよびそのオブジェクトからのインポート点において Copris と異なるなるツールになっている．

などの機能を利用しているが，これらの詳細について

以下では図 1 の流れに従って Scarab を説明する．

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

2 節では制約表現の部分にあたる Scarab プログラムと二つの問題記述例を説明する．次に与えられた制約

2. 2 Scarab DSL

集合を SAT 問題の節に符号化する方法を 3 節で述べ

Scarab DSL は Scala 上の埋込み DSL (embedded

る．4 節は SAT 問題に符号化された制約集合をどのDSL) として実装されている．CSP における項 (x + y

ようにして SAT ソルバーで解くかについて説明を行

等の数式) および制約 ((x > 0) ∨ (y > 0) 等の論理

い，Scarab の特長である Sat4j を用いた高度な解法式) を Scala 中で表現するために，次のようなクラについて説明を行う，5 節では性能評価を示す．

スを定義する: Term (項を表すクラス), Var (整数変数を表すクラス), Bool (ブール変数を表すクラス),

2 Scarab プログラム

Constraint (制約を表すクラス). これらのクラスはScarab を利用するための最も基本的な方法は Scarab
プログラムを記述することである．Scarab プログラムの記述には Scala と制約プログラミングのための†2 http://www.scala-lang.org/

Expr

CSP
1 variables: Sec [Var]

Term

Sum

Constraint

LiteralVarbools:dom:

Sec [Bool]
Map [Var, Domain]

1

1

1 constraints: Sec [Constraint]And

DomainOr

lb: Int
ub: Int

Not

Bool

LeZeroAssignment
11

図2

T ::= V-T

T + Int

T +T

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

And(C, . . . )op ::= <=

<

>=

===

Scarab における CSP クラス図T - Int

T -T

T * Int

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

And(Seq[C ])>intMap: Map[Var, Int]
boolMap: Map[Bool, Boolean]

C || C
Or(C, . . . )Or(Seq[C ])alldiff(Seq(T, . . . ))!==B ::= Bool(String, String, . . . )B (Any, . . . )図3Scarab における制約の構文規則

jp.kobe u.scarab.csp パッケージに属している．上記のクラスの関係を表したクラス図を図 2 に示す．
図 3 に Scarab DSL における制約の構文規則を

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)

示す．ここで T ，V ，C ，B は上述の Term，Var，

これらの整数変数を用いた制約 x ≤ 1 ∨ x1,2 ≤ 1 の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 は整数変数) の形に

Or が論理和，&& と And が論理積を表している．加Scarab DSL に お け る 制 約 定 義 の 例 を Scala

変換されるということである．線形制約のクラスはの REPL の 実 行 例 を 通 し て 説 明 す る (import

LeZero である．上記の例では x ≤ 1 ∨ x1,2 ≤ 1 は

jp.kobe u.scarab.csp. の実行を仮定している)．

x − 1 ≤ 0 ∨ x1,2 − 1 ≤ 0 に変換される．

整数変数を表すクラス Var は，変数名に加え文字列

この他に Scarab では Scala の暗黙変換を利用してのリストを添字として指定可能である．また，すでにシンボル (’ で始まる記号) を整数変数として利用である Var オブジェクトに任意の添字を追加した新しきるようになっており，次のように簡潔に制約を記述

い Var オブジェクトを作成できるように，apply メ

できる．

ソッドを定義している．

scala> ’y <= 0 || ’y(1,2) <= 0

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

val n = 15; val s =36
7

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

14

15

6

13

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

9

11

12

4

8

2

5
10
3 1

if (find) println(solution)
図4

SP (15, 36) の Scarab プログラムと計算された解

res2: jp.kobe_u.scarab.csp.Or =Or(LeZero(Sum(+y)),LeZero(Sum(+y(1,2))))

最後に Scarab DSL を用いた CSP の定義例を以下に示す．

ソッドを提供している．これによりデフォルトオブ
ジェクトに対する操作をオブジェクト名を陽に指定することなく簡潔に記述できるようになる．

2. 3. 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)

ら n まで 1 ずつ増加する正方形の集合を一辺の長さ s

このように定義された CSP の解を計算するためをそれぞれの正方形 i(1 ≤ i ≤ n) に (xi , yi ) がに CSP ソルバーのクラス Solver を用意している．

正方形 i の左下の座標を指すようにするものであSolver は jp.kobe u.scarab.solver パッケージにる．以下の制約は任意の二つの正方形 i と j (但し属しており, 定義された CSP の解を計算する find1 ≤ i < j ≤ n) が重なることを禁止する．
(xi + i ≤ xj )∨(xj + j ≤ xi ) ∨メソッドを提供している．find は与えられた CSP を

SAT に符号化し，SAT ソルバーを呼び出すことで解の計算を行う．Solver クラスおよび関係クラスについては後述する 4 節の図 8 も参考にされたい．

2. 3 Scarab プログラム例
本節では Scala と Scarab DSL を用いたプログラム(Scarab プログラム) の例を説明する．本節のプログ
ラム例では次のインポート文の実行を仮定している．
import jp.kobe u.scarab.csp.
import jp.kobe u.scarab.solver.
import jp.kobe u.scarab.sapp.

一つめの例は正方形詰込み問題を解くプログラムである．正方形詰込み問題 SP (n, s) は一辺の長さ 1 かの正方形の枠内に重なりなく配置する問題である．最も素直なモデリングは整数変数 xi , yi ∈ {0, . . . , s − i}(yi + i ≤ yj )∨(yj + j ≤ yi )図 4 に SP (15, 36) の時の Scarab プログラムを示す. Scarab DSL を用いることで簡潔に上記のモデルを表現できている．4，5 行目の int メソッドは整数変数をデフォルト CSP に定義している．ここで’x，’y は Scala におけるシンボルオブジェクトを表しており，前述のように Scala の暗黙変換により整数
変数オブジェクトへと変換される．9 から 12 行目のadd メソッドは上述の制約式を定義している．14 行
目の find メソッドは，定義された CSP を SAT へと符号化した後に解を計算，逆符号化している．逆符

ここで jp.kobe u.scarab.sapp は Scarab のアプリ号化された解は solution によって返され, Scala のケーションのためのシングルトンオブジェクトであprintln メソッドにより出力される．

り，CSP，CSP ソルバーそれぞれのデフォルトオブ
ジェクトや，それらに対する int, add, find 等のメ

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 プログラムと計算された解

2. 3. 2 汎対角線ラテン方陣
もう一つの例は CSP ソルバー競技会 [18] で使用さしている．この連言標準形の CSP におけるリテラル∑
は，ブール変数，ブール変数の否定， ni=1 ai xi ≤ c

れた汎対角線ラテン方陣 (Pandiagonal Latin Square)の形の線形制約のいずれかである．ここで ai は非零である．汎対角線ラテン方陣 P LS(n) は n 行 n 列の整数, c は整数値, そして xi は整数変数を表す. なの行列に 1 から n までの n 個の異なる整数を，各お連言標準形の CSP への変換は Tseitin 変換 [36] [32]整数が各行，各列，各汎対角線に 1 回だけ現れるよを用いて新しいブール変数を導入する方法で行ってうに配置する問題である．いま P LS(n) が与えらいる．

れたとき，整数変数を要素にもつ n 行 n 列の行列

xi,j ∈ {1, . . . , n} (1 ≤ i, j ≤ n) を用いてモデリング

以下では Scarab で採用している SAT 符号化である順序符号化とその実装について説明する．

を行う．各整数が 1 回だけ現れる制約は alldiﬀ 制約[26] によって表す．この制約は制約プログラミングの

3. 1 順序符号化分野で最もよく知られているグローバル制約の一つ

順序符号化法 [30] ではブール変数 p(x ≤ c) がそれであり，与えられた n 個の整数変数が互いに異なる

ぞれの整数変数 x と整数値 c ∈ {lb(x)−1, . . . , ub(x)}ことを意味する [37].

に対して導入される．ここで lb(x) と ub(x) はそれ

図 5 は P LS(5) に対する Scarab プログラムを表

ぞれ x の下限値と上限値である．さらに整数変数にしている. Scarab DSL は alldiﬀ を用いたモデリン

おける値の順序関係を表す以下の制約が導入される．

グを Scala の特長を用いて簡潔に表している．例えば 7 行目の alldiff(pos.map(j => ’x(i,j))) は各行においてそれぞれの変数が異なることを表す制約∧

ub(x)−1(¬p(x ≤ c − 1) ∨ p(x ≤ c))c=lb(x)+1

alldiﬀ (xi,1 , xi,2 , . . . , xi,n ) を表している．
順序符号化法では線形制約∑ni=1 ai xi≤ c を符3 Scarab における SAT 符号化

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

ここまで Scarab プログラムについて説明した．この変換を再帰的に適用し，変換式 (1a) と (1b) のこからは Scarab プログラムで記述された制約の SAT

x1 ≤ ⌊c/a1 ⌋ と x1 ≤ ⌈c/a1 ⌉ − 1 をそれぞれブール変符号化について説明する．

数 p(x1 ≤ ⌊c/a1 ⌋) と p(x1 ≤ ⌈c/a1 ⌉ − 1) に変換する

Scarab では与えられた CSP を，Simplifiler クラス (4 節の図 8 参照) の simplify メソッドを用いて前処理する．これによりまず連言標準形の CSP に変換

こ

ことで最終的に線形制約はブール変数上の連言標準形式へと変換される．


 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)(1a)(n = 1, a1 < 0)(1b)(n ≥ 2, a1 > 0)(1c)(n ≥ 2, a1 < 0)

(1d)

i=2

b=lb(x1 )図6

順序符号化における変換¬p(x2 ≤ 0) ∧
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 {(p(x1 ≤ 0) ∨ ¬p(x2 ≤ 1)) ∧(p(x1 ≤ 1) ∨ ¬p(x2 ≤ 2)) ∧case Seq((a,x)) =>(p(x1 ≤ 2) ∨ ¬p(x2 ≤ 3)) ∧if (a > 0) Seq(Seq(le(x, floorDiv(c, a))))p(x1 ≤ 3) ∧ p(x1 ≤ 4)
else Seq(Seq(le(x, ceilDiv(c, a)-1).neg))case Seq((a,x), axs1 @ _*) => {図 7 のように Scarab 中の順序符号化の中心部分
if (a > 0) {の実装は 20 行程度と非常にコンパクトであり，SAT
for {b <- lb(x) to ub(x)型システム開発者が SAT 符号化を変更し易いように
clause <- encodeLe(axs1, c-a*b)
なっている．図 8 のクラス図において SAT 符号化の} yield le(x, b-1) +: clause} else {仕様は Encoder という抽象クラスに記述されており，
for {
順序符号化は OrderEncoder に実装されている．こb <- lb(x) to ub(x)の Encoder クラスを実装することでこれまで提案さclause <- encodeLe(axs1, c-a*b)} yield le(x, b).neg +: clause
れてきた他の SAT 符号化を実装することも可能であ}る [14] [39] [11] [10] [1] [9] [35].
}}図7

順序符号化の実装

4 SAT ソルバー API と高度な解法
ここまで Scarab における制約記述，制約の SAT

3. 2 順序符号化の実装

符号化について 2 節，3 節で説明した．本節では SAT

図 7 は図 6 の変換を実装したプログラムを符号化された結果得られた SAT 問題を解くために用示 し て い る ．1 行 目 は 二 つ の 入 力 を 表 し て お り，いる抽象クラス SatSolver (図 8) についてまず説明{(a1 , x1 ), . . . , (an , xn )} と整数値 c である．5，6 行を行う．この API を通じた SAT ソルバーとの密な連目はそれぞれ変換式 (1a) と (1b) を表している．9

携は Scarab の大きな特長の一つとなっている．そのから 12 行目は変換式 (1c) を表している．11 行目で後インクリメンタル解法，仮説を用いた解法，制約のは {(a2 , x2 ), . . . , (an , xn )} と c − a1 b を入力としてコミットとロールバック，最適値の探索，組込み制約

encodeLe を再帰的に呼び出している．14 から 17 行などの高度な SAT 技術の利用について説明を行う．

目は同様に変換式 (1d) を表している．
例 と し て 正 方 形 詰 込 み 問 題 SP (2, 6) の 制 約 の

4. 1 SAT ソルバー API

一 部 で あ る 制 約 x1 + 1 ≤ x2 を 考 え る ．こ こ で

図 9 に SAT ソルバー API の一部を記述する．

x1 ∈ {0, . . . , 5} と x2 ∈ {0, . . . , 4} とする．まず初め

2 行目から 5 行目までは SAT ソルバーに制約をに x1 + 1 ≤ x2 は線形制約 x1 − x2 ≤ −1 に変形さ追加するメソッドになる．addClause は最も基本的れる. 図 7 の encodeLe を入力 {(1, x1 ), (−1, x2 )} となもので SAT 問題における節を SAT ソルバーへと−1 に入力として呼ぶことにより, 以下の順序符号化追加する．addAtLeast, addAtMost, addExactly はされた CNF 式が得られる:

基数制約を (SAT 符号化せずに) そのまま SAT ソル

1

CSP

1

1
1

Simplifier

8 参照)．Sat4j クラスは Java で実装された SAT ソ

SolverEncoder

ルバー Sat4j を用いて全てのメソッドを実装する．

1
1

Scarab と同一の JVM 上で Sat4j のインスタンスが作

SatSolver

成され全ての連携はメモリ上で行われる．ExtSolver

1

は外部 SAT ソルバー実行のためのクラスであり一1

OrderEncoder

図8

ExtSolver

Sat4j

Scarab におけるソルバークラス図 (一部)

部の基本的なメソッドのみを実装する．addClauseが呼ばれると問題ファイルに節の書き込みを行い，

isSatisfiable が呼ばれると SAT ソルバーが外部プ
ロセスとして起動され，問題ファイルの読み込みと求

1: abstract class SatSolver {2: def addClause(lits: Seq[Int])
3: def addAtLeast(lits: Seq[Int], degree: Int)
4: def addAtMost(lits: Seq[Int], degree: Int)
5: def addExactly(lits: Seq[Int], degree: Int)
6: def addConstr(c: org.sat4j.specs.Constr)
7: def isSatisfiable: Boolean
8: def isSatisfiable(assumps: Seq[Int]): Boolean
9: def model: Array[Int]10: def clearLearntClauses
11: def reset
... }
図9

SAT ソルバー API (一部)解を行う．C や C++で実装された最新の SAT ソル
バーを利用できることが利点であるが，Scarab との連携がファイル読み書きを通じて行われるためオーバヘッドが生じる．このことについては Java Native

Interface (JNI) や Java Native Access (JNA) を使うことで解決できるが，別途導入のコストがかかることになる．また最新の SAT ソルバーの多くは節以外の制約を利用できるような設計になっておらず，組込
み制約に関する機能は制限される．以降は SatSolverの全てのメソッドを実装可能な SAT ソルバー Sat4jの使用を仮定して説明を行う．

バーに追加する．これらのメソッドを実装する SAT
ソルバーでは組込みの基数制約を扱える必要がある．

4. 2 インクリメンタル解法

addConstr はユーザが定義した任意の組込み制約を

前節では SatSolver クラスについて説明した．本SAT ソルバーへと追加するメソッドである．組込み節では特にインクリメンタル解法について Scarab

基数制約, 組込み制約の応用については 4. 6 節と 4. 7

DSL からそれらが実際どのように利用出来るかを説節で説明する．

明する．

7，8 行 目 は 解 計 算 を 行 う メ ソッド で あ る ．

図 10 の 6〜9 行目に記載されるように, Scarab で

isSatisfiable は SAT ソルバーがメソッド実行時

は SAT ソルバーが一度解を計算した後でも制約の点で持っている制約を充足する解の存在を判定する.

追加が可能である．7 行目の 1 回目の find メソッド

Seq[Int]) も基本的なでは定義された CSP 全体が SAT 符号化され，生成動作は同じであるがリテラルの連言を仮説としてされた節集合が Sat4j へと追加される．次に SAT ソ

SAT ソルバーに与える点が異なる．SAT ソルバー

ルバー Sat4j が求解を行う．9 行目の 2 回目の find

isSatisfiable(assumps:

における仮説の扱いについては文献 [22] [7] が詳しメソッドでは 8 行目で追加された制約 x ̸= 3 のみがい．9 行目の model は問題が充足可能であることが符号化され，節集合が Sat4j に追加される．そして

isSatisfiable で判定された後に呼ぶことで充足解

Sat4j が再び求解を行う．

を返す．10 行目の clearLearntClauses は現時点で

ここで 1 回目の find メソッドによって生成された

保有している学習節を削除するメソッド，11 行目の学習節は 2 回目の呼び出し時にも保持されており，学

reset はソルバーの節や制約などの内部状態を初期

習節の再利用による効果的な解探索を期待できる (イ化するメソッドである．

ンクリメンタル解法)．但し，1 回目の CSP が充足不

現時点の Scarab では Sat4j クラスと ExtSolver
クラスが抽象クラス SatSolver を実装している (図能の場合には制約の追加は許可されないので注意さ4. 4 制約のコミットとロールバック
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// 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
図 10

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

Scarab では以下のような制約のコミット (commit)とロールバック (rollback) メソッドを提供している．

• commit メソッドは現在の CSP の状態 (整数変数，ブール変数，制約の数) を記録する．現在のScarab の実装では一つのコミットポイントを作成可能である．

• rollback メソッドは CSP を最後のコミットポ
イントの状態まで戻す．同時に Sat4j の状態もreset メソッドにより初期化されるので次回のfind メソッド呼び出し時には Sat4j へと節を追加し直す必要がある．
これら commit/rollback メソッドを実行すること
で，これまでに追加した制約の削除が可能となり，動的な制約の変更が必要なアプリケーションに対して，
より柔軟な解探索を提供することができると考えられる．しかし，符号化の手続きは繰り返し行う必要がれたい．

あり，CSP が充足不能になった場合には学習節は再利用できないので注意が必要である．

4. 3 仮説を用いた解法

図 10 の例では，16 行目でコミットポイントが生

Scarab DSL では制約を引数に持つ find(assump:

成され，17 行目で制約 x < y が追加されている．しConstraint) メソッドを用いることで CSP レベルでかし，この制約はこれまで追加された制約 (x = y)

仮説 (Assumption) に基づく解探索が可能である．但と矛盾するので充足不能が返される．次に 19 行目でし，現状は仮説に指定する制約はブール変数上のリテ

rollback メソッドが呼ばれ CSP が 16 行目の状態

ラルの連言に符号化される必要があり，それ以外の制まで戻される．すなわち制約 (x = y) が削除される．

約が指定された場合には例外が発生する．それぞれの20 行目で再び求解が行われ，この場合には CSP は充

リテラルは Sat4j へと渡されこの仮説リテラル集合

足可能となる．

に基づく SAT の解探索が Sat4j で行われる．
図 10 の例では，12 行目で仮説 y = 3 のもとで

4. 5 最適値の探索

CSP の求解が行われている．しかし，この仮説はこ

本節では上述の 3 つの機能を用いた応用として解れまで追加された制約 (x = y) ∧ (x ̸= 3) と矛盾すの最適化を紹介する．例として，図 4 に示した正方るので充足不能が返される．続いて仮説 x = 1 のも形詰込み問題 SP (n, s) について，制約を充足するよとで CSP の求解が行われ，この場合には充足可能とうな最小の正方形の枠の大きさを計算する．

なる．

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

このように仮説で指定した制約は CSP に永続的にラムを示している．このプログラムは図 4 のプログ追加されるのではなく，求解中にのみ有効であり，まラムの最下部に追加することで実行可能であり，プロ

た探索中に得られた学習節も保持される．後述するよ

グラム中の Scala の整数変数 n と s は図 4 で定義さうに，この仮説を用いた解法は最適解のデクリメンタ

れているものである．

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

まずプログラム 3 行目の整数変数 m ∈ {lb, . . . , ub}
は正方形の枠のサイズを表している．5，6 行目で定義される制約は全ての正方形がサイズ m の枠をはみ

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 (findNext)
println(solution)
図 11

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

出ないことを保証する．8 行目では find メソッドが

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

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

仮説 m ≤ ub とともに呼ばれている. もし解が存在するならば, 制約 m ≤ ub が追加され，ub が m の多く，CSP ソルバーにとっても重要な制約である．

最も最近の値から 1 つ小さい値に更新される (10 行

通常 SAT ソルバーはリテラルの選言である節の集目)．13，14 行目では全ての最適解が列挙されている．

合を入力として受け取るため，SAT ソルバーを用いてfindNext は最後に得られた解の否定をブロック節と解を求めるためには基数制約を節の集合に符号化する

して加えることで別の解の探索を行うようになって必要がある．基数制約の SAT 符号化は活発な研究分野いる．

の一つでありこれまで次のような方法が提案されてき図 12 は commit/rollback メソッドと制約の追加

た (括弧内は符号化節数): Binomial (n Ck+1 ), Total-を用いた二分探索を示している．6 行目は現在の下限

izer [2] (O(n·k)), Sequential Counter [27] (O(n·k)).

と上限のちょうど半分の値を計算している．7，8 行

Binomial と比較して Toalizer と Sequential Counter

目は正方形の枠の大きさを制限する制約を追加しては符号化節数が改良されているが，n と k が大きくいる．9 行目では, find メソッドが呼ばれている．もなるとやはり多くの節が出力される．

し CSP が充足可能である場合, 上限が更新され現在

Sat4j は他の多くの SAT ソルバーと異なり，節以外の CSP がコミットされる (10，11 行目). もし充足不の制約を Conflict Driven Clause Learning (CDCL)

能である場合, 下限が 1 だけ増加され最後のコミットの探索で扱うことが可能である．CDCL の詳細につポイントへと CSP がロールバックされる.

いては [22] に詳しい．本論文ではこのように SAT
ソルバー内で扱うことができる節以外の制約を組込

4. 6 組込み基数制約による符号化クラスの拡張

み制約と呼ぶ．Sat4j はこの組込み制約のためのイン

本節では 4. 1 節で説明した SatSolver クラスの中ターフェース Constr が用意されており，組込み基数

で特に addAtLeast, addAtMost, addExactly を用い制約は標準で実装されている組込み制約の一つであた SAT 符号化クラス OrderEncoder の拡張についてる．組込み基数制約は 4. 1 節に記載した addAtLeast,

説明する．

addAtMost, addExactly を使って Scarab から Sat4j

ブール基数制約 (以後，基数制約) とは，0-1 変数に入力される．

Scarab で は こ の 組 込 み 基 数 制 約 を 使った SATの値が 1 になるものに上限または下限を設定する制約∑であり， ni−1 xi ▷ k の形式のものをいう．但し，こ符 号 化 ク ラ ス NativeEncoder を 実 装 し て い る ．

こで i は整数変数, n は変数の数, k はしきい値を表

NativeEncoder は 3 節 で 説 明 し た SAT 符 号 化 ク

す整数とする．比較演算子 ▷ には ≤, ≥, = のいずれ

ラス OrderEncoder を継承しており, 基本的に順序符かが入る．基数制約で表現できる組合せ問題は非常に

表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号化を行うが基数制約を検知すると節へと符号化せる．propagate は監視中のリテラルの充足・非充足

ずに addAtLeast, addAtMost, addExactly メソッド

を基に値の伝播を行う．calcReason は矛盾が発生しを使って Sat4j に直接組込み基数制約を入力する．

た際に原因となった真偽値割当てをリテラルの連言とNativeEncoder は定義された CSP に基数制約がして生成する．最終的にこのように定義した制約は多く含まれている時に SAT ソルバーに追加される節

addConstr によって SAT ソルバーに追加することがの増加を抑えるため，符号化時間を短縮することとできる．

SAT ソルバーにおける単位伝播効率の悪化を防ぐこ

近年，論文 [6] のような節でない制約を SAT ソルとを期待出来る．NativeEncoder を使った場合の性バーに取り入れる研究がされているが，Scarab を用

能評価については 5. 2 節に記載する．

いることでこのような高度な SAT 技術の開発コストを少なくすることを期待できる．

4. 7 ユーザによる組込み制約の定義
前節では Sat4j における組込み基数制約とそれを用いた新しい SAT 符号化クラスについて説明を行った．ここではさらなる拡張として，組込み制約自体をユーザが定義する方法について説明する．

5 性能評価5. 1 汎対角線ラテン方陣
Scarab の基本性能を評価するために図 5 で示した
汎対角線ラテン方陣を用いて計算機実験を行った．こSatSolver クラスは addConstr メソッドを備えておこでは二つの alldiﬀ 制約の実装を用いた．一つめはり，これは Sat4j における org.sat4j.specs.Constr

naive 版で alldiﬀ 制約の定義に従い与えられた n 個∧の変数 x1 , . . . , xn の入力に対し， 1≤i<j≤n (xi ̸= xj )を実装した組込み制約を SAT ソルバーに追加する．
すなわち既に定義された基数制約だけでなく，ユーザが定義さえすれば任意の制約を SAT ソルバーで利用できるようになる．

なる制約を定義するものである．二つめは optimized∧∨n
版で，順列制約 ub
i=lb
j=1 (xj = i) と鳩ノ巣原理の∧∧制約 ¬ (xi < lb + n − 1) and ¬ (xi > ub − n + 1)

例えば図 14 は基数制約に係数 ai をつけた擬似ブー∑ル制約 ni−1 ai xi ▷ k を組込み制約として Scala 上でを naive 版に加えたものである．この鳩の巣原理の定義したプログラムを表している．一行目で Sat4j の版は Scarab では 2 行で実装されており optimizedorg.sat4j.specs.Constr を拡張して定義している版でも 15 行程度である．このように制約の実装をことに注意されたい．組込み制約を定義するために簡潔に記述でき，改良したものを実験できることはは大きく分けて register (10〜19 行目), propagate

Scarab で SAT 型システム開発を行う利点の一つで(21〜31 行目), calcReason (33 行目〜40 行目) の 3

ある．

制約の効果は文献 [29] で報告されている．なお naive

つのメソッドを定義するだけで良い．簡単に説明する

変換制限時間は 1 時間で，全ての計算時間は Xeonと register には制約が SAT ソルバーに追加された

2.93GHz の CPU，JVM に対して 2GB のメモリを時の動作を記述する．主に監視リテラルの設定にな割当てた MacOS X 上で行っている．

500[Velev ’09]
LKH 2.0.7
S4J-S (疎)S4J-S (密)S4J-N (密)Time (sec)

400

300

200

100

0
0

20

40

60

80

100

120

#Solved
図 13

Scarab 上に実装された CEGAR と NativeEncoder を使った HCP の解法 [28]

表 1 は P LS(n) (但 し 3 ≤ n ≤ 16) に 対 す る

されていく．SAT ソルバーは結果的に多くの回数起

Scarab の計算時間 (CPU 時間，秒) を示している．
optimized 版 alldiﬀ 制約を用いたものは n = 16 ま動する必要がある．本手法の詳細については論文 [28]とその補足ページ†3 を参照されたい．補足ページにでを解くことに成功している．2009 年に開催され記載があるが Scarab を使うことで本手法は問題の読た CSP ソルバー競技会では n ≤ 12 までを解いたみ込みも含めて 100 行程度で記述することができる．

Sugar を除くと n > 8 の P LS(n) を 1800 秒以内に比較に用いた手法は以下である．

どの CSP ソルバーも解くことができなかったことか

Velev 全制約を SAT 符号化する従来手法 [38]ら Scarab はこの問題において良い性能を示している

LKH DIMACS TSP チャレンジの全記録を保持する HCP/TSP ソルバー LKHといえる．

S4J-N (密) CEGAR + NativeEncoder
5. 2 ハミルトン閉路問題

S4J-S (密) CEGAR + Sequential Counter

ハミルトン閉路問題 (HCP) は与えられたグラフの

S4J-S (疎) S4J-S と同じ．しかし ExtSolver イ

全頂点を通る閉路を求める NP 完全問題である．グンターフェースで Sat4j を外部プロセスで起動しラフ理論における重要な問題であり，計算機科学におて疎な連携を模擬．

いても巡回セールスマン問題 (TSP) との関係があり

こ こ で S4J-S (密) と S4J-S (疎) は 両 方 と も重要である．本節では Scarab 上に実装された Coun-

OrderEncoder を用いて Sequential Counter を実装

terexample Guided Abstraction Refinement (CE-している．

GAR) [5] と NativeEncoder および OrderEncoder

図 13 は解いた問題数と CPU 時間 (カクタスプを使った HCP の解法の性能を論文 [28] の結果を用いロット) で各手法を比較したものである．結果よりて説明する．

S4J-N が最も右下にきており，最も高速に多くの問CEGAR を使って問題を解く場合，(i) 与えられた題を解いたことが分かる．HCP を CEGAR を用い問題はまず緩和され, (ii) 求解を行ったうえで誤った解が出力されればそれを修正するように制約が追加†3

http://kix.istc.kobe-u.ac.jp/~soh/scarab/jelia2014/

て解く場合には制約はほとんど基数制約になるためうことが可能である．Scarab が持つ制約表現および

NativeEncoder を用いる S4J-N が OrderEncoder を用

SAT 符号化モジュールとこれら Sat4j の機能の組合せ

いた Sequential Counter を実装した S4J-S (密) よりは SAT 技術のさらに応用を広げることを期待できる．

も良い結果となった．また実装が異なる S4J-S (密)Scarab の情報とソースコードは以下から入手できる.

と S4J-S (疎) の実験結果の違いは SAT ソルバーを複

http://kix.istc.kobe-u.ac.jp/~soh/scarab/.

数回起動する CEGAR メソッドを使った場合の起動コストとファイル読み書きによるオーバヘッドの影

参 考 文 献響が小さくないことを表しており，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 Applicationsof Satisfiability Testing (SAT 2004), LNCS 3542,
2004, pp. 1–15.
[ 2 ] Bailleux, O. and Boufkhad, Y.: Eﬃcient CNF
Encoding of Boolean Cardinality Constraints, Proceedings of the 9th International Joint Conference
on Principles and Practice of Constraint Programming (CP 2003), LNCS 2833, 2003, pp. 108–122.
[ 3 ] 番原睦則, 田村直之: SAT によるシステム検証, 人
工知能学会誌, Vol. 25, No. 1(2010).
[ 4 ] 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.
[ 5 ] Clarke, E. M., Grumberg, O., Jha, S., Lu, Y.,
and Veith, H.: Counterexample-Guided Abstraction
Refinement, CAV, 2000, pp. 154–169.
[ 6 ] Dvorák, W., Järvisalo, M., Wallner, J. P., and
Woltran, S.: Complexity-sensitive decision procedures for abstract argumentation, Artif. Intell.,Vol. 206(2014), pp. 53–78.
[ 7 ] Eén, N. and Sörensson, N.: Temporal Induction
by Incremental SAT Solving, Electronic Notes in
Theoretical Computer Science, Vol. 89, No. 4(2003).
[ 8 ] Ganesh, V., O’Donnell, C. W., Soos, M., Devadas, S., Rinard, M. C., and Solar-Lezama, A.:
Lynx: A Programmatic SAT Solver for the RNAFolding Problem, SAT, 2012, pp. 143–156.
[ 9 ] 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.
[10] 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.
[11] Gent, I. P.: Arc Consistency in SAT, Proceedings of the 15th European Conference on Artificial
Intelligence (ECAI 2002), 2002, pp. 121–125.
[12] Hebrard, E., O’Mahony, E., and O’Sullivan, B.:
Constraint Programming and Combinatorial Optimisation in NumberJack, Proceedings of CPAIOR,
2010, pp. 181–185.
[13] 井上克巳, 田村直之: SAT ソルバーの基礎, 人工知SAT ソルバーと密に連携するシステムで実装することの重要性を示している．全制約をまず最初に全て

SAT 符号化する Velev と S4J-N の違いは顕著であり
CEGAR のような高度な SAT 解法の必要性が読み取れる．また最新の TSP ソルバーである LKH と比較しても S4J-N は高速に多くの問題を解いている．
最後に上記で使われた問題から構造的な問題を多く含む color04 (119 問) を用いて Sugar と C++で実装された Minisat を内部に持つ Copris で CEGARと Sequential Counter を実装して解いたところ制限
時間 500 秒以内に 84 問を解いた．S4J-N は同じ制限
時間内に 86 問を解いており良い性能を示している．

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

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

Scarab の興味深い拡張の一つとして Sat4j の機能をさらに導入することがある. 例えば Sat4j は与えられた

CNF 式が充足不能である時に Minimal Unsatisfiable
Subformula (MUS) を計算することが可能である. 加
えて埋め込みの最適化メソッドおよび解列挙メソッド，
また基数制約や擬似ブール制約なども入力として扱

能学会誌, Vol. 25, No. 1(2010).
[14] Iwama, K. and Miyazaki, S.: SAT-Variable
Complexity of Hard Combinatorial Problems,Proceedings of the IFIP 13th World Computer
Congress, 1994, pp. 253–258.
[15] Janota, M., Grigore, R., and Marques-Silva,
J.: Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription,
JELIA, 2010, pp. 195–207.
[16] Janota, M., Klieber, W., Marques-Silva, J., andClarke, E. M.: Solving QBF with Counterexample
Guided Refinement, SAT, 2012, pp. 114–128.
[17] Le Berre, D. and Parrain, A.: The Sat4j library, release 2.2, Journal on Satisfiability, Boolean
Modeling and Computation, Vol. 7, No. 2-3(2010),
pp. 59–6.
[18] Lecoutre, C., Roussel, O., and van Dongen,
M. R. C.: Promoting Robust Black-box Solvers
Through Competitions, Constraints, Vol. 15,
No. 3(2010), pp. 317–326.
[19] 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.
[20] Metodi, A. and Codish, M.: Compiling finite domain constraints to SAT with BEE, TPLP, Vol. 12,
No. 4-5(2012), pp. 465–483.
[21] 鍋島英知: SAT によるプランニングとスケジューリ
ング, 人工知能学会誌, Vol. 25, No. 1(2010).
[22] 鍋島英知, 宋剛秀: 高速 SAT ソルバーの原理, 人工知能学会誌, Vol. 25, No. 1(2010).
[23] 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳:
パッキ ン グ 配 列 問 題 の 制 約 モ デ リ ン グ と SAT 符 号
化, コンピュータソフトウェア, Vol. 31, No. 1(2013),
pp. 116–130.
[24] Odersky, M.: The Scala Experiment ― Can We
Provide Better Language Support for Component
Systems?, 2006.
[25] Odersky, M., Spoon, L., and Venners, B.: Programming in Scala, Artima, Inc., second edition,
2010.
[26] 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.
[27] Sinz, C.: Towards an Optimal CNF Encodingof Boolean Cardinality Constraints, Proceedings ofthe 11th International Joint Conference on Principles and Practice of Constraint Programming (CP2005), LNCS 3709, 2005, pp. 827–831.
[28] 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.
[29] 田島宏史: SAT 変換に基づく制約ソルバーの高速化に関する研究, 修士論文, 神戸大学大学院自然科学研究科, 2006.
[30] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Constraints, Vol. 14, No. 2(2009), pp. 254–272.
[31] 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.
[32] 田村直之, 丹生智也, 番原睦則: SAT 変換に基づく
制約ソルバーとその性能評価, コンピュータソフトウェ
ア, Vol. 27, No. 4(2010), pp. 183–196.
[33] 田村直之, 丹生智也, 番原睦則: 制約最適化問題とSAT 符号化, 人工知能学会誌, Vol. 25, No. 1(2010).
[34] 田村直之, 丹生智也, 番原睦則: Scala 上の制約プロ
グラミング用ドメイン特化言語 Copris について, コン
ピュータソフトウェア, Vol. 29, No. 4(2012), pp. 114–
129.
[35] 丹生智也, 田村直之, 番原睦則: 位取り記数法に基づく整数有限領域上の制約充足問題のコンパクトかつ効率的な SAT 符号化, コンピュータソフトウェア, Vol. 30,
No. 1(2013), pp. 211–230.
[36] Tseitin, G. S.: On the complexity of derivationsin the propositional calculus, Studies in Mathematics and Mathematical Logic Part II, (1968), pp. 115―–125.
[37] van Hoeve, W.-J. and Katrie, I.: Global
Constraint, Handbook of Constraint Programming,
Foundations of Artificial Intelligence, Elsevier,
2006, pp. 169–208.
[38] Velev, M. N. and Gao, P.: Eﬃcient SAT Techniques for Relative Encoding of Permutations with
Constraints, Australasian Conference on Artificial
Intelligence, 2009, pp. 517–527.
[39] Walsh, T.: SAT v CSP, Proceedings of the 6thInternational Conference on Principles and Practice of Constraint Programming (CP 2000), 2000,
pp. 441–456.
[40] 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.

1: class NativePB(voc: ILits, ps: IVecInt, coef: Seq[Int], degree: Int)
extends Constr with Propagatable with Undoable {2: val maxUnsatisfied = coef.sum - degree
3: var counter = 0
4: var remains: Set[Int] = Set.empty
5: var coefMap: Map[Int, Int] = Map.empty
6: val lits = new Array[Int](ps.size)
7: ps.moveTo(this.lits)
8: register9:
10: def register {11:
for (i <- 0 until lits.size) {12:
voc.watch(lits(i) ^ 1, this)13:
coefMap = coefMap + ((lits(i) >> 1) -> coef(i))
14:
if (voc.isFalsified(lits(i))) {15:
voc.undos(lits(i) ^ 1).push(this)16:
counter += coef(i)
17:
}
18:
}
19: }
20:
21: def propagate(s: UnitPropagationListener, p: Int): Boolean = {22:
voc.watch(p, this)23:
if ((counter + coefMap(p >> 1)) > maxUnsatisfied) return false
24:
counter += coefMap(p >> 1)
25:
voc.undos(p).push(this)26:
27:
for (q <- lits if voc.isUnassigned(q) && ((counter + coefMap(q >> 1)) > maxUnsatisfied))28:
if (!s.enqueue(q, this))29:
return false
30:
true
31: }
32:
33: def calcReason(p: Int, outReason: IVecInt) {34:
var c = 035:
for (q <- lits if voc.isFalsified(q)) {36:
outReason.push(q ^ 1)37:
c += coefMap(q >> 1)
38:
if (c > maxUnsatisfied) return
39:
}
40: }
図 14

組込み擬似ブール制約の定義 (一部)