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

制約解集合プログラミングシステムの設計方式に関す
る考察
宋 剛秀

則武 治樹

番原 睦則

田村 直之

井上 克巳

解集合プログラミング (Answer Set Programming; ASP) は，一階述語論理に基づいた論理型プログラミング言語の一種である．記号上の探索問題を簡潔に記述できることが特長の一つであるが，算術的な制約を直接表現する
ことはできない．一方，制約プログラミング (Constraint Programming; CP) は算術的な制約を対象としている．
このような背景から ASP と CP の統合が注目を集めており，両者の機能を併せ持つ制約解集合プログラミング(Constraint Answer Set Programming; CASP) が研究されるようになった．本論文では CASP システムの一構成方式について考察する．ここでは，CASP システム muﬃn を ASP システム上に実装する．muﬃn の CASP 言
語のベースは ASP であり，ASP の記号的な制約の記述に加えて算術的な制約の記述が可能である．また ASP の記
号や項を変数名やコレクション名として用いることができるため，簡潔な問題記述が可能である．これまで提案されてきた CASP システムと異なり，muﬃn は前処理方式とライブラリ方式を融合したシステムであることにも特長がある．論文では実装した muﬃn を用いた基礎実験の結果についても報告を行う．

Answer Set Programming (ASP) is a logic programming based on the first order logic, which has a rich yet
simple modeling language for symbolic constraints. However, it is not so well to represent arithmetic andglobal constraints for which Constraint Programming (CP) has a suited language. To integrate advantegesof both programming paradigms, Constraint Answer Set Programming (CASP) has been studied. In thispaper, we consider a design of CASP systems and its implementation called muﬃn. The CASP languageof muﬃn is based on ASP and can represent arithmetic and global constraints in addition to symbolic constraints. Symbols and terms in ASP can be represented by names of variables and collections in muﬃn.
Another feature is the translation between CASP and ASP: it is processed by using pre-processing and ASP
library. We also report preliminaly experiments on muﬃn.

容は基礎から応用にまで及び，近年の論理プログラミ

1 はじめにングに関する国際会議 (ICLP) においても，ASP に

解集合プログラミング (Answer Set Program-関する発表は非常に多く，この分野における主要なト

ming; ASP) [21] は，一階述語論理に基づいた論理

ピックの 1 つとなっている．

型プログラミング言語の一種である．ASP は Prolog

ASP の研究内容は基礎的な研究だけにとどまらず，等の従来の論理型プログラミング言語の拡張として，実際的な応用まで様々である，近年の成功例として

2000 年頃から活発に研究されてきた [12] [29]．研究内

は，その記述力と ASP ソルバーの性能を活かして，Studies on a Design of Constraint Answer Set Programming Systems
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura,
神戸大学情報基盤センター, Information Science andTechnology Center, Kobe University.
Haruki Noritake, 神戸大学大学院システム情報学研究
科, Graduate School of System Informatics, Kobe
University.
Katsumi Inoue, 国立情報学研究所, National Instituteof Informatics.

ASP を時間割問題に適用した研究がある [5]．この研究では時間割問題が解集合プログラムによって簡潔に記述でき，その解が ASP ソルバーによってシミュ
レーティド・アニーリング法などの，従来研究と比較しても高速に計算されることが報告されている．
その他の ASP の特徴を以下に述べる．

• 知識表現言語として優れ，扱える問題は標準論
理プログラムを用いる場合はクラス N P ，選言論

理プログラムの場合はクラス∑P2に属する [13]．

• 安定モデル意味論に基づいたモデルの探索・列挙が行える．

• 記述言語は非 Horn 節である．
• 一階述語形式で問題を記述可能で，与えられた問題を自然・簡潔に記述できる．

• 演繹データベース，論理プログラミング，非単調推論を起源としている [21]．

ル制約が紹介されている．
その他の CSP の特徴を以下に述べる．

• N P 完全問題に属する．
• 研究・応用が活発に行われている [8] [10] [18] [19][22] [23] [31] [34] [35] [37] [38]．

• 様々なソルバーが開発されており，中でも SAT型システムが成功を収めている．特に，SAT 型
制約ソルバーの Sugar [33] †2 が 2008–2009 年国• ASP ソルバーの開発が活発に行われている．

際 CSP ソルバー競技会において 2 年連続優勝

特 に 与 え ら れ た ASP を 基 礎 化 す る ソ ル バ ー(GLOBAL 部門) する等の実績を残している．

gringo [11] [14] と基礎化された ASP から解集

• 共通の制約モデリング言語がなく，ソルバー合を求める clasp [16] が事実上の標準となっていに よ り 異 な る ．な お ，上 記 の 国 際 CSP ソ ル

る．この他に Cmodels [27] は ASP を充足可能性

バー競技会においては，XML 形式で記述された判定 (SAT) 問題に変換して求解を行う SAT 型

CSP(XCSP) が用いられている．

システムである．

• どの言語も算術制約やグローバル制約の記述性

制約充足問題 (Constraint Satisfaction Prob-は保証されているが，配列を扱う構文が存在しな

lem; CSP) は，各変数に与えられたドメインからい．また，項を変数として扱うことができない．

値を割り当てることで，与えられた制約のすべてをここまで述べたように，ASP と CSP はそれぞれ満たすことができるかどうかを判定する問題である

異なる特長を持っている．ASP は記述言語として優[7] [9]．すべての制約を満たす値割り当てが存在する

れており，複雑な問題を簡潔に記述することができる

場合，元の CSP は充足可能 (SAT) であるといい，そが，算術的な記述やグローバル制約に関しては CSPの値割り当てが解となる．値割り当てが存在しないの方が優れている．しかし，それぞれの言語はソル

場合，元の CSP は充足不能 (UNSAT) であるという．

バーの系統が全く異なり，互いの問題を扱うことがで

本論文では CSP を整数の有限領域上の問題として扱

きない．そのため，各々の良い点を統合した言語およう．制約には算術論理演算等で記述されるものの他

びソルバーの開発が注目を集めている [26]．

に，alldiﬀerent 等に代表されるいわゆるグローバル
制約がある．

制約解集合プログラミング (Constraint Answer

Set Programming; CASP) は，解集合プログラ

グ ロ ー バ ル 制 約 (global constraint) は ，複ミングをベースとし，さらに制約プログラミング分

数 の 変 数 に 対 す る 複 雑 な (し か し 意 味 の あ る)

野で活発に研究されている算術制約やグローバル制

条 件 を 簡 潔 に 表 す た め に 導 入 さ れ た ．例 え ば ，約の処理を兼ね備えたプログラミング言語である．

alldiﬀerent(x1 , x2 , . . . , xn ) は，xi が互いに異なるこ

両方の利点を兼ね備えることにより，グローバル制とを表す．xi ̸= xj を個別に記述するよりも簡潔に約を含んだ規模の大きな問題を，ASP や CSP と比なり，また効率の良い解法アルゴリズムの存在が知較して簡単な構文で扱うことができる．これまでいられている [20]．このようなグローバル制約は，記述

くつか ASP と CSP の両方に関わる研究がされてい性および効率性の向上を目的として制約ソルバーやる [30] [12] [3] [1] [2] [15] [28]. これらの包括的なサーベ制約プログラミングシステムに数多く取り入れられイとしては論文 [26] が詳しい．上記に挙げた中でも特ている．これらのグローバル制約を集約した Global
Constraint Catalog †1 には，300 以上のグローバに CASP システム実現している clingcon [30] は ASP†1 http://www.emn.fr/z-info/sdemasse/gccat/

言語を拡張して算術制約を取り扱えるようにしてお†2 http://bach.istc.kobe-u.ac.jp/sugar/

り，制約ソルバーと ASP ソルバーをハイブリッドにるが，整数変数，算術制約，グローバル制約を記述で実行することで解を求める．CASP システム inca [12]きるようにする．

も ASP 言語を算術制約を扱えるようにした拡張言語

本論文では CASP 言語のベースとして ASP の記述を入力とするところは clingcon と同じであるが，初言語である標準論理プログラム (Normal Logic Pro-期の inca については入力を全て ASP の記号制約に

gram; NLP) を用いる．詳細については文献 [13] [21]

符号化してから ASP ソルバーによって求解する前処に詳しいがここでは簡単に説明を行う. NLP は以下

理方式を取るという特徴がある．

の形式のルールの集合として構成される．

本論文では CASP システムの一構成方式として従L1 ← L2 , . . . , Lm , not Lm+1 , . . . , not Ln

来の ASP 言語の述語を用いて算術制約を記述し，前

ここで m ≥ n ≥ 0 であり, Li は正または負のリテラ処理方式によって求解する方法を提案する．特に符号ルで, not はデフォルトの否定, “,” は連言を表す．こ化アプローチの部分については算術制約の処理に ASPのルールにおいて ← の左部をルールのヘッド，右側で記述されたライブラリを用いており，今後の開発でをルールのボディと呼ぶ．ボディが空のルールをファ別の符号化方法を少ないコストで導入可能であるこクトと呼び，ヘッドが空のルールを制約と呼ぶ．

とが特長である．提案する CASP システムの実装と以上が NLP におけるルールの簡単な説明である．

して muﬃn を開発した．muﬃn は順序符号化 [34] [35]上記に加えていくつかの ASP ソルバーでは組合せ問を用いて算術制約およびグローバル制約を ASP の記

題を ASP で解くために便利なアグリゲート (aggre-

号制約へと符号化する．順序符号化は国際 CSP ソルgate) と呼ばれる表記法がいくつか用意されている．

バー競技会の優勝ソルバーである Sugar [33] にも採用

これらの詳細についても文献 [13] [21] に詳しい.

されており，前処理方式に組込むことで muﬃn の高速な求解を期待出来る．

2. 1 CASP 言語の設計

muﬃn の性能を評価するための部分実験を行った．

本研究で提案する CASP 言語の設計方針は上述の

muﬃn は CASP システムであるので，ASP, CSP,

ASP をベースにするということ，整数変数，算術制

CASP の問題を入力とすることができるが，今回は約，グローバル制約を記述できるようにするというこ

CSP の問題をベンチマークとして用いて，CSP にとの 2 点である．本研究では ASP 上の述語を用いて対する muﬃn の性能を調査する．この理由は ASP

これらの方針に基づいた言語を実現する．提案するにおいて muﬃn で採用しているバックエンドのソル

CASP の基礎となる述語と意味は以下になる．

バー gringo と clasp の性能は既に過去の ASP ソル• variable(V, int(LB, UB))

バー競技会 [17] の結果より十分に証明されているこ

ドメインの上限下限が UB と LB となる整数変数と，CASP についてはまだ研究途上であり十分な数

V の定義．

のベンチマークがないことである．よって今回は部• collection(C, X)

分実験として国際 CSP ソルバー競技会で用いられた変数または制約 X がコレクション C に属するこ1797 問を用いて行った結果について報告を行う．

との定義．

以下では，第 2 節 CASP システムの設計方式につ• constraint(A)いて述べ，第 3 節でその実装である muﬃn の説明を

制約 A の定義．

行う．第 4 節では muﬃn の基本性能の評価実験の結果について説明する．

特に collection の導入によりグローバル制約を
特定のコレクション変数に対して適用だけで，そのコレクション変数に属する全ての変数と制約に適用出2 CASP システムの設計来るようになるという利点がある．constraint で定本研究では, CASP システムの実現方法として符号義される制約 A は，表 1, 表 2, 表 3, 表 4 の述語を組化アプローチをとる．入力言語は ASP をベースにすみ合わせたものである．なおここでは算術制約，比較

表1

算術制約

表4

グローバル制約

述語

意味

述語

意味

neg(X)−X

alldiﬀerent(X1, X2, ...)

X1 , X2 , . . . は全てadd(X1, X2, ..)X1 + X2 + . . .

sub(X1, X2, ..)X1 − X2 − . . .

mul(X1, X2)

X1 × X2

div(X1, X2)

X1 /X2

mod(X1, X2)

X1 を X2 で割った余り

min(X1, X2)

X1 と X2 の小さい値

max(X1, X2)

X1 と X2 の大きい値
表2

比較制約

述語

意味

eq(X1, X2)

X1 = X2

ne(X1, X2)

X1 ̸= X2

le(X1, X2)

X1 ≤ X2

lt(X1, X2)

X 1 < X2

ge(X1, X2)

X1 ≥ X2

gt(X1, X2)

X 1 > X2
表3

異なる値であるpredicate((P, Xs), (P(Xs)))

P(Xs) を定義 (Xs ⇔X1 , X2 . . . )1: (int x11 1 9)
2: (int x12 1 9)...
9: (int x33 1 9)
10: (= (+ x11 x12 x13) 15)
11: (= (+ x21 x22 x23) 15)
12: (= (+ x31 x32 x33) 15)
13: (= (+ x11 x21 x31) 15)
14: (= (+ x12 x22 x32) 15)
15: (= (+ x13 x23 x33) 15)
16: (= (+ x11 x22 x33) 15)
17: (= (+ x13 x22 x31) 15)
18: (alldifferent x11 x12 x13 x21x22 x23 x31 x32 x33)
図1

Sugar CSP による 3 × 3 の魔方陣の記述

論理制約

述語

意味

not(L)¬L

and(L1, L2, ..)L1 ∧ L2 ∧ . . .

or(L1, L2, ..)L1 ∨ L2 ∨ . . .

imp(L1, L2)

L1 → L2

xor(L1, L2)

L1 , L2 の排他的論理和

iﬀ(L1, L2)

L1 , L2 の同値関係

if(L, T, F)

論理式 L が成り立つなら T ，異なるなら F

制約，論理制約，グローバル制約を区別して記述する
が，以下では特に問題がない場合には記号制約との

1: #const n = 3.
2: #const sum = n*(n*n+1)/2.
3: num(1..n).
4: variable(x(I,J), int(1,n*n)) :- num(I), num(J).
5: collection(xs, x(I,J)) :- num(I), num(J).
6: collection(row(I), x(I,J)) :- num(I), num(J).
7: collection(col(J), x(I,J)) :- num(I), num(J).
8: collection(d1, x(I,I)) :- num(I).
10: collection(d2, x(I,n-I+1)) :- num(I).
11: constraint(alldifferent(collection(xs))).
12: line(row(I)) :- num(I).
13: line(col(J)) :- num(J).
14: line(d1;d2).
15: constraint(eq(add(collection(L)), sum)) :line(L).
図2

CASP を用いた 3 × 3 の魔方陣の記述

対比としてこれらの制約を総称して算術制約と呼ぶ．
述語の中で可変長引数 X1 , X2 , . . . を引数に取るもの

2. 2 CASP を用いた魔方陣の記述

はコレクション変数を引数にして記述する事ができ

魔方陣は n × n の行列について，縦・横・斜めのる．また，表 4 のグローバル制約については一例でいずれについても，数字の合計が同じになるようにあり，後述の Sugar(3. 1 節) で読み込めるグローバル1 ∼ n2 の異なる数字を配置する問題である．例えば

制約を記述することが可能である．

x(1, 1), x(1, 2) . . . x(3, 3) の 3 × 3 行列について考える場合には縦・横・斜めのいずれについても，総和が15 になるように各 x に 1 ∼ 9 のそれぞれ異なる値を割当てる．
図 1 は Sugar CSP の，図 2 は CASP の 3 × 3 の魔方陣に対する記述である．CSP の 18 行に対し，

CASP は 14 行で記述することができる．
また n × n の魔方陣について考える場合，CSP で記述すると n2 + 2n + 3 の行数が必要になるが，CASP
ならば 3 × 3 の場合と同様に 14 行だけで記述する事ができる．さらに，魔方陣のサイズを変える場合，

1: (int a 0 1)
2: (int b 0 1)
3: (int c 0 1)
4: (int d 0 1)
5: (int e 0 1)
6: (<= (+ (* 3 a) (* 4 b) (* 5 c)(* 7 d) (* 9 e)) 15)
7: (>= (+ (* 4 a) (* 5 b) (* 6 c)(* 8 d) (* 10 e)) 19)
図3

Sugar CSP によるナップサック問題の記述

CSP は全体的に書きなおす必要があるが，CASP は
図 2 の 1 行目の変数を変えるだけで対応できる．また，CSP と比べて CASP は項をそのまま変数として記述している．例えば (2, 1) のマスの変数を記述するとき，CSP では x21 となるのに対し，CASP では

x(2, 1) と分かりやすく記述することができる．
2. 3 CASP を用いたナップサック問題の記述
ナップサック問題とはある容量 C を持つナップサッ
クと値段と価値の対によって表される n 種類の品物が与えられた時に，容量 C を超えない範囲で価値の和が最大になるように品物を選ぶ問題である．ここでは例として以下のような品物 a, b, c, d, e と容量

C = 15 が与えられた時に，価値が 19 以上になるよ
うな組合せを求める問題を考える．

1: #const ub_price = 15.
2: #const lb_value = 19.
3: item(a, 3, 4).
4: item(b, 4, 5).
5: item(c, 5, 6).
6: item(d, 7, 8).
7: item(e, 9, 10).
8: variable(x(Item), int(0,1)) :item(Item, Price, Value).
9: collection(prices, mul(Price,x(Item))) :item(Item, Price, Value).
10: collection(values, mul(Value,x(Item))) :item(Item, Price, Value).
11: constraint(le(add(collection(prices)), ub_price)).
12: constraint(ge(add(collection(values)), lb_value)).
図4

名前

a

b

c

d

e

容量

3

4

5

7

9

価値

4

5

6

8

10

この問題は Sugar CSP では図 3，CASP では図 4のように記述できる．CSP は算術制約が得意であCASP を用いたナップサック問題の記述

2. 4 CASP 処理系の設計
設計の指針を以下に示す．

• ASP では CSP の記述は扱えないため，算術制
約やグローバル制約といった CSP の記述部分を分割し，処理を行う．

り，ナップサック問題については簡潔に書けるが，変• グローバル制約には可変長引数を扱う制約も多数が増えたり条件が変わると全体的に書きなおす必

いが，ASP 上では可変長引数を扱う制約を記述

要がある点は魔方陣と同様である．一方，CASP はすることは難しい上に動作が遅いため，ASP 外

item(e, 9, 10). までの行がインスタンスであり，で変換を行う．

それ以降がモデリングである．値段や価値の上限や下限といった条件を変数，(名前，値段，価値) の組の要

• ソルバーや符号化法を交換可能なシステムにする．

素を item として記述しており，モデリングが書けてこのシステムの利点は，従来のソルバーや正規化手法

いれば条件や要素が変わっても分かりやすく書き換えの良いところを少ない開発コストで利用できることることができる．

である．また，算術制約を処理するライブラリを書き換えることで他の符号化法に変更したり，ASP ソル

ASP(算術制約なし)

算術制約処理ライブラリ

CASP

正規化された制約

算術制約( 3) ASPソルバー実行( 2) 算術制約の正規化(1) 分離図5

解CASP システムの設計方式

解

CASP
ASP
(算術制約なし)

順序符号化
ライブラリ

基礎化されたCASP(1) CASPの基礎化
gringo

正規化された制約

算術制約(2) 分離shell( 3) 算術制約の正規化
Sugar

図6

基礎化された
ASP

算術制約を表す
ASPの述語( 4) ASP述語への変換
Prolog( 6) ASPソルバー実行
clasp( 5) ASPの基礎化
gringoCASP システム muﬃn の構成

バーを交換することで様々な ASP ソルバーをそのま構文に対して ASP の述語が書いてあることも多ま利用することが可能である．

い．設計した CASP の構文は gringo で読み込め

図 5 に提案する CASP システムの設計方式を示す．

るようになっているため，まずは gringo で述語

1. CASP を ASP の部分と CSP の部分に分割する．

の解釈を行う．

2. CSP を，算術制約を処理するライブラリと ASP• ASP と CSP の分離

ソルバーの組み合わせで読み込めるような ASP

CSP と し て 処 理 す る 部 分 が variable，に変換する．

collection，constraint の 3 つで記述がまと3. 2 つの ASP とライブラリと組み合わせ，ASP
ソルバーで求解する．
上記の手順により CASP の解を ASP ソルバーによって求める．

めてあるため，シェルの grep を用いることにより簡単に分離できる．

• 分離した CSP 部分の正規化
Sugar を用いる．Sugar は SAT 型の CSP ソル
バーであるが，CSP を正規化して出力する機能

3 CASP システム muﬃn の実装もある．Sugar を用いるメリットとして以下の要

3. 1 全体の処理

素が挙げられる．

図 6 に実際に実装したシステムを示す．なお CSP– 明らかに不要な探索範囲の削減や，可変長と ASP 間の変換は今回は Prolog を用いて行った．

引数の制約とグローバル制約を全て 3 項以

• CASP の正規化
CASP は CSP と ASP が混在しており，CSP の下の制約に正規化する機能がある．この機能により，ASP で可変長引数を扱う点について考慮する必要がなくなる．また，ASP のみで処理するよりも高速である．

– CASP だけでなく，Sugar CSP や XCSP も読み込める．

下の節を追加する．

¬p(z ≤ 0) ∨ p(z ≤ 1)¬p(z ≤ 1) ∨ p(z ≤ 2)

この時，上記の節を充足可能にする真理値割り当ては

4 通りあり，それぞれ z = 0, z = 1, z = 2, z = 3 に– Sugar が改良された際にはそのまま流用できる．

• 算術制約処理ライブラリの実装

対応する．

p(z ≤ 0)p(z ≤ 1)p(z ≤ 2)

解釈

1

1

1

z=0

0

1

1

z=1

0

0

1

z=2

0

0

0

z=3

算術制約を処理する方法として，以下のような符号化法がこれまでに提案されている．

– 直接符号化法 [10] [31] [38]– 順序符号化法 [34] [35]– 支持符号化法 [19] [23]制約については，制約に違反する範囲を符号化す– 対数符号化法 [18] [22]ればよい．一般の線形制約については，以下のよう

今回のシステムでは，順序符号化法 (Order En-

coding; OE) を用いて算術制約処理ライブラリを実装する (以下 oe.lp と参照)．順序符号化法の内容については後述する．順序符号化法は，求解になる．今，ai を非零の整数定数，c を整数定数，zi を互いに異なる整数変数とする．この時，制約∑ni=1 ai zi ≤ c は以下のように符号化できる．

困難な問題として知られるショップ・スケジュー∧∨リング問題，二次元矩形パッキング問題，組合せΣni=1 bi =c−n+1i

テストのテストケース生成問題に対して，未知の最適値を決定するなど優れた性能を示している [4] [6] [24] [25] [32] [34]．また，単位伝播に優れ∑
ここで bi は， ni=1 bi = c − n + 1 を満たすように動くとし，変換 ()# は以下のように定義する．

ており，記号上の制約として扱う上で高い効果が得られる．

(a z ≤ b)#• ASP ソルバー
ASP を正規化する gringo と，SAT ソルバーとしても動作する clasp の組み合わせを用いる．

(ai zi ≤ bi )#≡ p(z ≤ ⌊b/a⌋)(a > 0)¬p(z ≤ ⌈b/a⌉ − 1) (a < 0)
ただし，z の取り得る最小値未満の a については
p(z ≤ a) を偽に変換し，最大値以上については真に変換する．例えば，整数変数 w, z のドメインが3. 2 順序符号化法{0, 1, 2, 3} の時，制約 w − z ≤ −1 は以下の 4 つの節

順序符号化法 [34] [35] では，各整数変数 z につに符号化される．

いて，そのドメインが {a1 , a2 , . . . , an } の時 (ただし

a1 < a2 < . . . < an )，z ≤ ai を表す n − 1 個の命
題変数 p(z ≤ a1 ), p(z ≤ a2 ), . . . , p(z ≤ an−1 ) を用いる．なお，z ≤ an は常に真であるため，命題変数p(z ≤ an ) は不要である．また，これらの命題変数間の関係を表す以下の節を用いる．

¬p(z ≤ ai ) ∨ p(z ≤ ai+1 )(1 ≤ i ≤ n − 2)

例えば，変数 z のドメインが {0, 1, 2, 3} の場合，3 つの命題変数 p(z ≤ 0), p(z ≤ 1), p(z ≤ 2) を用い，以¬p(z ≤ 0)p(w ≤ 0) ∨ ¬p(z ≤ 1)p(w ≤ 1) ∨ ¬p(z ≤ 2)p(w ≤ 2)
ここで，p(w ≤ 0) ∨ ¬p(z ≤ 1) は「w ≤ 0 または
z > 1」であること，すなわち「w ≥ 1 かつ z ≤ 1」が制約に違反する領域であることを表している．
図 7 に w − z ≤ −1 の充足領域を表す．制約を満たす点は •，違反点は × でプロットされている．

w ̸= z の場合，一旦 w − z ≤ −1 ∨ z − w ≤ −1 のように線形制約に置き換え，さらに Tseitin 変換を用

% le0/2: X <= c:- le0(X,C), not p(X,C), dom(X,C).
:- le0(X,C), lb(X,LB), C < LB.
% lt0/2: X < cle0(X,C-1) :- lt0(X,C).

図7

w − z ≤ −1 の解領域を表したグラフ

dom(V,LB..UB) :- var(V), lb(V,LB), ub(V,UB).
{ p(V,A) : dom(V,A) } :- var(V).
:- p(V,A), not p(V,A+1), dom(V,A+1), var(V).
:- not p(V,UB), var(V), ub(V,UB).
図8% gt0/2: X > c:- gt0(X,C), p(X,C), dom(X,C).
:- gt0(X,C), ub(X,UB), C >= UB.
% ge0/2: X >= c
gt0(X,C-1) :- ge0(X,C).
% eq0/2: X == cle0(X,C) :- eq0(X,C).
ge0(X,C) :- eq0(X,C).

整数変数とドメインの定義

いて (p ∨ q) ∧ (¬p ∨ w − z ≤ −1) ∧ (¬q ∨ z − w ≤ −1)% ne0/2: X != c
1 { gt0(X,C), lt0(X,C) } :- ne0(X,C).

と変換してから符号化する (p，q は新しい命題変数)．

図9

したがって w ̸= z は以下の 9 個の節に符号化される．

比較制約の定義p∨q¬p ∨ ¬p(z ≤ 0)

¬q ∨ ¬p(w ≤ 0)¬p ∨ p(w ≤ 0) ∨ ¬p(z ≤ 1)

¬q ∨ p(z ≤ 0) ∨ ¬p(w ≤ 1)

¬p ∨ p(w ≤ 1) ∨ ¬p(z ≤ 2)

¬q ∨ p(z ≤ 1) ∨ ¬p(w ≤ 2)

¬p ∨ p(w ≤ 2)

¬q ∨ p(z ≤ 2)

順序符号化法では，直接符号化，支持符号化，対数符号化等と比較し，より短い節が生成される．また，
順序符号化法で生成した節に対しては，単位伝播が整数制約上での範囲伝播に対応することが知られている [36]．

3. 3 算術制約処理ライブラリの実装% le0/3: aX <= c:- le0(A,X,C), A>0, C>0, not p(X,D), dom(X,D),
D=C/A.
:- le0(A,X,C), A>0, C<0, not p(X,D), dom(X,D),
D=(C-A+1)/A.
:- le0(A,X,C), A<0, C>0, p(X,D-1), dom(X,D),
D=C/A.
:- le0(A,X,C), A<0, C<0, p(X,D-1), dom(X,D),
D=(C+A+1)/A.
:- le0(A,X,C), A==0, C<0.
:- le0(A,X,C), A>0, C==0, not p(X,0), dom(X,0).
:- le0(A,X,C), A<0, C==0, p(X,-1), dom(X,-1).
:- le0(A,X,C), A>0, lb(X,LB), A*LB>C.
:- le0(A,X,C), A<0, ub(X,UB), A*UB>C.

3. 2 節で述べたような順序符号化を実装するために
図 10

ASP 上で次のように定義を行う．
変数とドメインの定義 (図 8).

1 行目は変数 V ，上限 U B ，下限 LB が事実として記述されると，対応するドメイン dom(V,A) (LB ≤ A ≤ U B) が定義されることを示している．2 行目でそれぞれの変数 V に対して，dom(V,A) を満たすような V, A の組全てに対し，命題変数 p(V,A) が定義される．ASP では:より左側を空節にすると右側の否定条件になるため，3 行目は ¬p(V, A) ∨ p(V, A + 1) を表している．また，4 行目は上限のドメイン p(V, U B) が常に真であることを示している．

制約 AX ≤ C の定義

等号，不等号の定義 (図 9).

X を変数，C を定数とする．

• X ≤ C (le0/2) : 1 行 目 は X ≤ C な ら ばp(X, C) が真であること，2 行目は C が下限未満の値であれば定義が成り立たないことを表している．

• X < C (lt0/2) : X ≤ C を用いて定義される．
• X > C (gt0/2) : 1 行 目 は X > C な ら ばp(X, C) が偽であること，2 行目は C が上限以上の値であれば定義が成り立たないことを表して

% ge0/3: aX >= cle0(MA,X,MC) :- ge0(A,X,C), MA=(-1)*A, MC=(-1)*C.
% eq0/3: aX == cle0(A,X,C) :- eq0(A,X,C).
ge0(A,X,C) :- eq0(A,X,C).
% le/5: aX+bY <= c (aX <= c - bY)
le0(A,X,C) :- le(A,X,0,Y,C).
le0(A,X,T) :- le(A,X,B,Y,C), B<0, p(Y,DY), dom(Y,DY), T=(C-B*DY).
le0(A,X,T) :- le(A,X,B,Y,C), B>0, not p(Y,DY-1), dom(Y,DY), T=(C-B*DY).
% ge/5: aX+bY >= cle(MA,X,MB,Y,MC) :- ge(A,X,B,Y,C), MA=(-1)*A, MB=(-1)*B, MC=(-1)*C.
% eq/5: aX+bY == cle(A,X,B,Y,C) :- eq(A,X,B,Y,C).
ge(A,X,B,Y,C) :- eq(A,X,B,Y,C).
% le/7: aX+bY+cZ <= d (aX + bY <= d - cZ)
le(A,X,B,Y,D) :- le(A,X,B,Y,0,Z,D).
le(A,X,B,Y,T) :- le(A,X,B,Y,C,Z,D), C<0, p(Z,DZ), dom(Z,DZ), T=(D-C*DZ).
le(A,X,B,Y,T) :- le(A,X,B,Y,C,Z,D), C>0, not p(Z,DZ-1), dom(Z,DZ), T=(D-C*DZ).
% ge/7: aX+bY+cZ >= dle(MA,X,MB,Y,MC,Z,MD) :- ge(A,X,B,Y,C,Z,D), MA=(-1)*A, MB=(-1)*B, MC=(-1)*C, MD=(-1)*D.
% eq/7: aX+bY+cZ == dle(A,X,B,Y,C,Z,D) :- eq(A,X,B,Y,C,Z,D).
ge(A,X,B,Y,C,Z,D) :- eq(A,X,B,Y,C,Z,D).
図 11

3 項制約の定義なく負の可能性もあり，小数点以下を切り捨てる際に不都合が生じる．故に A と C が正か負か，あるいは% false causes unsat.
:- false.

0 かで細かく場合分けして記述する必要がある．
3 項以下の線形制約の定義 (図 11).

% remove domain:- p(V,A-1), not p(V,A), remdom(V,A).
:- not p(V,A-1), p(V,A), remdom(V,A).

AX ≥ C ，

AX ̸= C については AX ≤ C を用いて定義する．また，2 項と 3 項の線形制約についても，それぞれ 1 項

図 12と 2 項の線形制約を使うことにより簡潔に定義でき追加で必要な定義

る．ただし，係数の正負により場合分けをする必要が
いる．

ある．

• X ≥ C (ge0/2) : X > C を用いて定義される．

その他の留意すべき点 (図 12).

• X = C (eq0/2) : X ≤ C ∧ X ≥ C で定義．

理で明らかに制約を満たせないことが分かった場合，• X ̸= C (ne0/2) : X < C ∨ X > C で定義．

Sugar の出力は false. のみとなるため，false. が

1 項の線形制約 (AX ≤ C) の定義 (図 10).

XをSugar による処偽であるという制約を書いておく必要がある．

変数，A と C を定数とする．定数同士の四則演算はまた，変数が離散的に定義される事も考慮する必要が直接記述しても問題はない．AX ≤ C を単純に変形ある．例えば V ∈ {1 . . . 4，7 . . . 10} の場合である．

すると X ≤ C/A であるが，ドメインが正だけでは

変数 V の欠けているドメイン I を定義から取り除くと

:-p(x(1,1),1),not p(x(1,1),2).
:-p(x(1,1),2),not p(x(1,1),3).
...
:-p(x(1,1),8),not p(x(1,1),9).
:-not p(x(1,1),9).
図 13x(1, 1) の基礎化例

le(1,x(1,1),1,x(2,1),6):-not p(x(3,1),8).
le(1,x(1,1),1,x(2,1),7):-not p(x(3,1),7).
le(1,x(1,1),1,x(2,1),8):-not p(x(3,1),6).
le(1,x(1,1),1,x(2,1),9):-not p(x(3,1),5).
le(1,x(1,1),1,x(2,1),10):-not p(x(3,1),4).
le(1,x(1,1),1,x(2,1),11):-not p(x(3,1),3).
le(1,x(1,1),1,x(2,1),12):-not p(x(3,1),2).
le(1,x(1,1),1,x(2,1),13):-not p(x(3,1),1).
le(1,x(1,1),1,x(2,1),14).
図 14x(1, 1) + x(1, 2) + x(1, 3) ≤ 15) の基礎化例:-le0(1,x(1,1),9),not p(x(1,1),9).
:-le0(1,x(1,1),1),not p(x(1,1),1).
:-le0(1,x(1,1),2),not p(x(1,1),2).
:-le0(1,x(1,1),3),not p(x(1,1),3).
:-le0(1,x(1,1),4),not p(x(1,1),4).
:-le0(1,x(1,1),5),not p(x(1,1),5).
:-le0(1,x(1,1),6),not p(x(1,1),6).
:-le0(1,x(1,1),7),not p(x(1,1),7).
:-le0(1,x(1,1),8),not p(x(1,1),8).
図 16x(1, 1) ≤ C の基礎化例

3. 4 gringo による算術制約の基礎化
gringo で，3. 3 節の oe.lp と，CASP から生成された 2 つの ASP コードを読み込んで正規化 ASP を生成する．
整数変数の宣言は，oe.lp により対応するドメインと命題変数が生成される．例えば，var(x(1,1)). lb(x(1,1), 1). ub(x(1,1), 9).
について生成される ASP 式は，図 13 のようになる．
le0(1,x(1,1),-1) :le(1,x(1,1),1,x(2,1),8),not p(x(2,1),8).
le0(1,x(1,1),0) :le(1,x(1,1),1,x(2,1),8),not p(x(2,1),7).
le0(1,x(1,1),1) :le(1,x(1,1),1,x(2,1),8),not p(x(2,1),6).
le0(1,x(1,1),2) :le(1,x(1,1),1,x(2,1),8),not p(x(2,1),5).
le0(1,x(1,1),3) :le(1,x(1,1),1,x(2,1),8),not p(x(2,1),4).
le0(1,x(1,1),4) :le(1,x(1,1),1,x(2,1),8),not p(x(2,1),3).
le0(1,x(1,1),5) :le(1,x(1,1),1,x(2,1),8),not p(x(2,1),2).
le0(1,x(1,1),6) :le(1,x(1,1),1,x(2,1),8),not p(x(2,1),1).
le0(1,x(1,1),7) :le(1,x(1,1),1,x(2,1),8).
図 15x(1, 1) + x(2, 1) + x(3, 1) ≤ 15) の基礎化例

線形制約については，それ自身は一時変数と同様に変数記号として扱われる．制約内に線形制約が存在する場合，gringo により変数割り当てが総当りで行われ，命題変数に関わる制約式が自動生成される．
例えば，

x(1, 1) + x(2, 1) + x(3, 1) ≤ 15について，まず 3 項制約の定義により x(3, 1) のそれ
ぞれの場合について 2 項制約を生成する (図 14)．次に，一例として x(3, 1) > 6 の場合について考える．
すなわち x(1, 1) + x(2, 1) ≤ 8 が成り立つ場合，さらに x(2, 1) のそれぞれの場合について 1 項制約を生成する (図 15)．1 項制約については安易に命題変数の制約に置換ができる (図 16)．
このように算術制約を記号上の制約に落としこむ
ことで，CSP の要素を ASP として扱い，求解するこきは remdom(V,I) と定義し，順序符号化法においてとが可能となる．生成される制約が膨大になるが，順は p(V, I) と p(V, I − 1) が同値関係になるように処理

序符号化法は制約伝播に優れているため，ほとんどのする．例の場合だと，var(V). lb(V,1). ub(V,10).

制約は高速で処理することができる．

の後に，remdom(V,5). remdom(V,6). を定義する．

4 CSP を用いた部分実験
実装した muﬃn の基本性能を評価するための CSPを用いた部分実験を行った．

muﬃn は CASP システムであるので，ASP, CSP,

600

CASP の問題を入力とすることができるが，今回はjumpy
trendyfrumpy500

CSP の問題をベンチマークとして用いた．この理由
400

CPU時間(秒)は ASP において muﬃn で採用しているバックエンドのソルバー gringo と clasp の性能は既に過去の ASP

300

200

ソルバー競技会 [17] の結果より十分に証明されている

100

こと，CASP についてはまだ研究途上であり十分な

0

数のベンチマークがないことである．よって今回は国

0

10

20

30

40

50

60

70

80

90

100

解けた問題数

際 CSP ソルバー競技会で用いられた問題によって部
図 17分実験を行う．

clasp の動作モードの比較

以下の実験において実験環境は Linux マシン (CPU3.0GHz， メモリ 6GB)，問題の変換からソルバーに600

よる求解までの全体のタイムアウトは 600 秒とした．

500

Sugar
muffin

CPU時間(秒)400

4. 1 clasp の動作モードの選択
今回設計した muﬃn で用いる clasp には数種類の

300

200

動作モードがあり，muﬃn で運用する上でどの動作

100

モードが最も適しているのかを調査するための実験を

0
0

200

400

行った．ベンチマークとして 2009 年の国際 CSP ソ
ルバー競技会のベンチマーク問題から外延的制約を

600

800

1000

1200

1400

解けた問題数

図 18

CSP 競技会ベンチマーク 1707 問の実験結果除いた問題 (1797 問) から，各シリーズごとに 3 問ずつ選択した 174 問を用いた．

ドと比較しても常にほぼ右下にある，また frumpy と

こ れ ら の 問 題 に 対 し ，muﬃn を 用 い て ，trendy が解いた問題は全て jumpy でも求解ができた

clasp2.1.3†3 において標準で提供されている 3 つのため，muﬃn の評価実験を jumpy で行うことにする．

動作モードに対し実験を行った: frumpy は clasp のデ
フォルトの動作モードで，汎用的な用途に用いられ

4. 2 部分実験の結果

る．jumpy は探索のリスタートを頻繁に行い，充足可CSP Solver Competition(2009) のベンチマーク問

能な問題に強い．trendy は構造的な問題に対して効

題から外延的制約を除いた全ての問題 1797 問を用果的に働く．

いて評価実験を行った．これらの問題に対し，muﬃn

ベンチマーク問題は XCSP で書かれており，Sugarと Sugar の 2 通りで実験を行った．Sugar は SAT 型

で読み込めるため，muﬃn でも求解が可能である．

CSP ソルバーであり，SAT ソルバーを用いて求解

図 17 に実験結果のカクタスプロットを示す．カクを行う．今回は muﬃn との比較のために clasp を用タスプロットの横軸は解けた問題数を，縦軸は昇順にいる．また，clasp の動作モードは前節の結果より，並び替えたソルバーの CPU 時間を示している．すな

muﬃn, Sugar ともに jumpy に設定する．

わち，この表はグラフが右にあるほど多くの問題を解

実験結果の解けた問題数と CPU 時間を比較するたき，下にあるほど高速に求解していることを示す．結めに，図 18 にカクタスプロットを示す．解けた問題

果として，frumpy が 88 問，jumpy が 94 問，trendy

数については，muﬃn が 1209 問，Sugar が 1397 問が 93 問求解しており，また jumpy は他の動作モーであった．XCSP 問題は CSP ソルバーに向けて作られたベンチマークのため直接の比較は困難であるが，†3 http://www.cs.uni-potsdam.de/clasp/

求解数について，muﬃn は Sugar の 87%程度の性能

600

500

500

400

400

Sugar

Sugar

600

300

300

200

200

100

100

0

0
0

100

200

300

400

500

600

0

100

200

muffin

図 19

ソルバー求解時間の比較

図 20

500

600

1200

1400

符号化時間の比較

Sugar
muffinうために，図 19 にスキャッタープロットを示す．ス

400

CPU時間(秒)また，実験結果について詳しく Sugar との比較を行

500

キャッタープロットの横軸は muﬃn の CPU 時間を，縦軸は Sugar の CPU 時間を示している．スキャッ

300

200

タープロットの中心の直線より右下に点が集中してい100るため，Sugar の方が全体的に動作が速いが，左上の00方にもいくつかまとまってプロットが存在しており，か存在する．

400

600となっている．

muﬃn の方が Sugar よりも動作が速い問題がいくつ300

muffin

200

400

600

800

1000

解けた問題数

図 21

符号化でタイムアウトした問題を除く CSP 競技会
ベンチマーク 1322 問の実験結果

ASP が CSP より部分的に優れている点についてより詳しく考察する．問題をシリーズごとに分けた求解数と動作時間の平均を表 5 と表 5 に示す．

換中にタイムアウト，もしくはメモリ不足になった
問題数について調べると，Sugar は 10 問しかなかっ

動作時間の平均については，解けなかった問題をタたのに対し，muﬃn は 475 問もあった．さらに，変イムアウトの 600 秒に換算して算出している．これら

換が正常に終了している問題に限定したカクタスプの表を見ると，All Interval Series, Pseudo-Boolean

ロットを図 21 に示す．図 21 は図 18 と比べると，大(fpga のみ), Queen Attacking, Social Golfers に限っ

幅に差が縮まっていることが分かる．また，gringo のては muﬃn の方が優れていることが分かった．これ前までの変換は全てタイムアウトまでに終わっておらは変数 1 つあたりのドメインの範囲が小さな問題

り，muﬃn の変換過程で最も動作時間がかかるのはが多い．ドメインの範囲が小さな問題が得意な理由とgringo であることが確認されている．gringo が最も遅しては，ドメインが小さいと整数を扱う制約と記号的い原因は，CSP をより規模の大きな問題である ASP

な制約のギャップが小さくなり，gringo の動作が高速に変換しているためだと考えられる．gringo に処理になる点が考えられる．

させる ASP の記述を改善することで，大幅な性能上

一方，Cabinet, FAPP については 1 問も解けなかっ昇が見込める．

た．これらは変数のドメインがかなり欠けている問題

今後の課題としては，算術制約処理ライブラリのであり，remdom の処理にかなりの時間がかかってし記述の改善が挙げられる．例えば 2 項以上の制約をまったためだと考えられる．

1 項少ない制約に変換するとき，現状では決められた

次に，遅くなる原因についても考察する．図 20 に順序で展開しているが，この時の順序を探索範囲が少CSP から clasp で処理する直前の基礎化 ASP への変

なくなるように条件分岐で変更すると gringo で生成換にかかった時間のスキャッタープロットを示す．変

される制約の数が軽減される．

表5

Series2D Strip Packing (20)All Interval Series (15)BIBD (83)
BMC (15)
BQWH (20)Cabinet (40)
Chessboard Coloration (15)
Costas Array (11)Cumulative Job-Shop (10)Domino (10)
FAPP (120)
Fischer (25)
Golomb Ruler (28)Graph Coloring (141)
Haystacks (15)
Job-Shop (76)Knights (10)Langford (43)
Latin Square (10)Magic Square (18)Multi Knapsack (6)NengFa (10)Open-Shop (75)Perfect Square Packing (74)
Pigeons (29)
Primes (76)Pseudo-Boolean-GLB (100)
Pseudo-Boolean-fpga (15)Pseudo-Boolean-others (248)
Quasigroup Existence (35)
Queen Attacking (10)Queens (25)
RCPSP (78)
RLFAP (59)Rader Surveillance (65)
Ramsey (16)Schurr’s Lemma (10)Social Golfers (10)Super-solutions (85)Timetabling (46)muﬃn
457.45219.94106.89
54.31
2.01
600
142.57171.46368.9
107.58600
454.68290.6
204.02493.9
166.02346.58255.8961.52
410.71
269.4947.44
124.17310.17124.44319.26208.7925.84
187.71104.27368.44270.32
3.69
133.294.7
285.54122.33250.68254.14206.11

各シリーズ毎の平均 CPU 時間

Sugar
340.2
253.68
39.6
15.78
1.53
18.53
130.2
162.76366
68.38
369.05313.63266.37197.18490.4
106.64260.4252.7661.13
300.49166.5314.84
46.9
183.83124.43236.87180.15299.76140.6697.21
383.1
149.91
1.7
6.14
1.7
270.6
104.29251.06193.86111.94

Series2D Strip Packing (20)All Interval Series (15)BIBD (83)
BMC (15)
BQWH (20)Cabinet (40)
Chessboard Coloration (15)
Costas Array (11)Cumulative Job-Shop (10)Domino (10)
FAPP (120)
Fischer (25)
Golomb Ruler (28)Graph Coloring (141)
Haystacks (15)
Job-Shop (76)Knights (10)Langford (43)
Latin Square (10)Magic Square (18)Multi Knapsack (6)NengFa (10)Open-Shop (75)Perfect Square Packing (74)
Pigeons (29)
Primes (76)Pseudo-Boolean-GLB (100)
Pseudo-Boolean-fpga (15)Pseudo-Boolean-others (248)
Quasigroup Existence (35)
Queen Attacking (10)Queens (25)
RCPSP (78)
RLFAP (59)Rader Surveillance (65)
Ramsey (16)Schurr’s Lemma (10)Social Golfers (10)Super-solutions (85)Timetabling (46)Solved (1797)

muﬃn
5
10
74
15
20
0
12
8
4
9
0
11
16
98
3
59
5
26
9
6
4
10
70
39
23
41
75
15
178
30
4
17
78
55
65
9
8
6
53
39
1209

Sugar
10
9
80
15
20
40
12
9
4
10
64
16
16
99
3
66
6
26
9
10
5
10
71
56
23
47
73
8
196
30
4
20
78
59
65
10
9
6
62
41
1397

数をまとめて 1 つのコレクション変数として扱える5 まとめようにする．また CASP システムの言語処理系の設

本論文では，ASP と CSP の利点を統合した CASP

計方針は次の２つである．(a) 算術的な制約やグロー

システムの設計方式について提案を行った．提案する

バル制約といった CSP の記述部分を分割し，ASP 外CASP システムにおける言語の設計方針は次の２つで正規化する．(b) 各機能をモジュール化し，符号化である．(a) まず ASP の記述言語が拡張され，算術ライブラリやソルバーを容易に変更可能にする．

的な制約やグローバル制約を含む規模が大きな問題

また提案した CASP システム設計方式の実装としについても簡潔に記述可能にする．(b) いくつかの変てを muﬃn を開発した．muﬃn は近年成功を収めている順序符号化を用いて開発した符号化ライブラリと，最新の ASP ソルバーを用いて実装した．
実装した CASP システム muﬃn については CSP
競技会で使われた 1797 問の CSP を使って部分実験を行い CSP 問題に対する基本性能についても評価を行った．muﬃn は ASP, CSP, CASP の問題を入力とすることができるが，今回 CSP をベンチマークとして用いた理由は CASP がまだ研究途上であり広範なベンチマークの整備がされていないこと，バックエン
ドの ASP ソルバー gringo と clasp は ASP において既に高い性能が示されていることである．muﬃn の

CSP に対する今後の課題としては，作成した符号化ライブラリの記述の改良を行うことによる符号化にかかる時間の短縮を行うことが考えられる．またベンチマーク整備も CASP 研究分野の課題として挙げられる．

参 考 文 献[ 1 ] Balduccini, M. and Lierler, Y.: ASP-Based
Problem Solving with Cutting-Edge Tools, ICLP2011 Workshop on Answer Set Programming andOther Computing Paradigms (ASPOCP 2011),
2011, pp. 14–28.
[ 2 ] Balduccini, M. and Lierler, Y.: Practical andmethodological aspects of the use of cutting-edge
ASP tools, Practical Aspects of Declarative Languages, Springer, 2012, pp. 78–92.
[ 3 ] Banbara, M., Gebser, M., Inoue, K., Schaub,T., Soh, T., Tamura, N., and Weise, M.: Aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming, CoRR,
Vol. abs/1312.6113(2013).
[ 4 ] Banbara, M., Matsunaka, H., Tamura, N., andInoue, K.: Generating Combinatorial Test Cases byEﬃcient SAT Encodings Suitable for CDCL SAT
Solvers, Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-17), 2010, pp. 112–
126.
[ 5 ] Banbara, M., Soh, T., Tamura, N., Inoue, K.,
and Schaub, T.: Answer set programming as amodeling language for course timetabling, TPLP,
Vol. 13, No. 4-5(2013), pp. 783–798.
[ 6 ] Banbara, M., Tamura, N., and Inoue, K.: Generating Event-Sequence Test Cases by Answer Set
Programming with the Incidence Matrix, TechnicalCommunications of the 28th International Conference on Logic Programming (ICLP 2012), Dovier,A. and Costa, V. S.(eds.), LIPIcs, Vol. 17, Schloss
Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012,

pp. 86–97.
[ 7 ] Barták, R.: On-line Guide to Constraint Programming, http://kti.ms.mff.cuni.cz/~bartak/
constraints/, 1998.
[ 8 ] Béjar, R., Hähnle, R., and Manyà, F.: A Modular Reduction of Regular Logic to Classical Logic,
Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logic (ISMVL 2001),
2001, pp. 221–226.
[ 9 ] Bordeaux, L., Hamadi, Y., and Zhang, L.:
Propositional Satisfiability and Constraint Programming: A Comparative Survey, ACM Computing Surveys, Vol. 38, No. 4(2006).
[10] de Kleer, J.: A Comparison of ATMS and CSP
Techniques, Proceedings of the 11th International
Joint Conference on Artificial Intelligence (IJCAI1989), 1989, pp. 290–296.
[11] Delgrande, J. and Faber, W.(eds.): Proceedingsof the Eleventh International Conference on Logic
Programming and Nonmonotonic Reasoning (LPNMR’11), Lecture Notes in Artificial Intelligence,Vol. 6645, Springer-Verlag, 2011.
[12] Drescher, C. and Walsh, T.: A translational
approach to constraint answer set solving, TPLP,
Vol. 10, No. 4-6(2010), pp. 465–480.
[13] Gebser, M., Kaminski, R., Kaufmann, B., andSchaub, T.: Answer Set Solving in Practice, Synthesis Lectures on Artificial Intelligence and Machine Learning, Morgan and Claypool Publishers,
2012.
[14] Gebser, M., Kaminski, R., König, A., andSchaub, T.: Advances in gringo Series 3, In Delgrande and Faber [11], pp. 345–351.
[15] Gebser, M., Hinrichs, H., Schaub, T., andThiele, S.: xpanda: A (simple) preprocessor for
adding multi-valued propositions to ASP, Proceedings of the 23rd Workshop on (Constraint) Logic
Programming 2009, Universitätsverlag Potsdam,
2010, pp. 51.
[16] Gebser, M., Kaufmann, B., Neumann, A., andSchaub, T.: Conflict-Driven Answer Set Solving,
Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), 2007,
pp. 386–.
[17] Gebser, M., Liu, L., Namasivayam, G., Neumann, A., Schaub, T., and Truszczynski, M.: The
First Answer Set Programming System Competition, LPNMR, 2007, pp. 3–17.
[18] Gelder, A. V.: Another Look at Graph Coloring via Propositional Satisfiability, Discrete Applied
Mathematics, Vol. 156, No. 2(2008), pp. 230–243.
[19] Gent, I. P.: Arc Consistency in SAT, Proceedings of the 15th European Conference on Artificial
Intelligence (ECAI 2002), 2002, pp. 121–125.
[20] Gent, I. P., Miguel, I., and Nightingale, P.:
Generalised Arc Consistency for the AllDiﬀerent
Constraint: An Empirical Survey, Artificial Intelligence, Vol. 172, No. 18(2008), pp. 1973–2000.

[21] 井上克巳, 坂間千秋: 論理プログラミングから解集合
プログラミングへ, コンピュータソフトウェア, Vol. 25,
No. 3(2008), pp. 20–32.
[22] Iwama, K. and Miyazaki, S.: SAT-Variable
Complexity of Hard Combinatorial Problems,Proceedings of the IFIP 13th World Computer
Congress, 1994, pp. 253–258.
[23] Kasif, S.: On the Parallel Complexity of Discrete
Relaxation in Constraint Satisfaction Networks, Artificial Intelligence, Vol. 45, No. 3(1990), pp. 275–
286.
[24] 越村三幸, 鍋島英知, 藤田博, 長谷川隆三: SAT 変換
による未解決ジョブショップスケジューリング問題への挑戦, スケジューリング・シンポジウム 2009 講演論文集, 2009, pp. 209–213.
[25] Koshimura, M., Nabeshima, H., Fujita, H., andHasegawa, R.: Solving Open Job-Shop Scheduling
Problems by SAT Encoding, IEICE TRANSACTIONS on Information and Systems, Vol. E93-D,
No. 8(2010), pp. 2316–2318.
[26] Lierler, Y.: Relating constraint answer set programming languages and algorithms, Artif. Intell.,Vol. 207(2014), pp. 1–22.
[27] Lierler, Y. and Maratea, M.: Cmodels-2: SATbased answer set solver enhanced to non-tight programs, Logic Programming and Nonmonotonic Reasoning, Springer, 2004, pp. 346–350.
[28] Liu, G., Janhunen, T., and Niemelä, I.: Answer
Set Programming via Mixed Integer Programming,
KR, 2012.
[29] Niemelä, I.: Answer Set Programming: A
Declarative Approach to Solving Search Problems,
JELIA, Fisher, M., van der Hoek, W., Konev, B.,
and Lisitsa, A.(eds.), Lecture Notes in Computer
Science, Vol. 4160, Springer, 2006, pp. 15–18.
[30] Ostrowski, M. and Schaub, T.: ASP modulo

CSP: The clingcon system, TPLP, Vol. 12, No. 45(2012), pp. 485–503.
[31] Selman, B., Levesque, H. J., and Mitchell, D. G.:
A New Method for Solving Hard Satisfiability Problems, Proceedings of the 10th National Conference on Artificial Intelligence (AAAI 1992), 1992,
pp. 440–446.
[32] Soh, T., Inoue, K., Tamura, N., Banbara, M.,
and Nabeshima, H.: A SAT-based Method for Solving the Two-dimensional Strip Packing Problem,
Fundamenta Informaticae, Vol. 102, No. 3–4(2010),
pp. 467–487.
[33] Tamura, N. and Banbara, M.: Sugar: a CSP to
SAT Translator Based on Order Encoding, Proceedings of the 2nd International CSP Solver Competition, 2008, pp. 65–69.
[34] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Proceedings of the 12th International Joint Conference on Principles and Practice of Constraint Programming (CP 2006), LNCS 4204, 2006, pp. 590–
603.
[35] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Constraints, Vol. 14, No. 2(2009), pp. 254–272.
[36] 田村直之, 丹生智也, 番原睦則: 制約最適化問題とSAT 符号化, 人工知能学会誌, Vol. 25, No. 1(2010),
pp. 77–85.
[37] Tanjo, T., Tamura, N., and Banbara, M.: A
Compact and Eﬃcient SAT-Encoding of Finite Domain CSP, Springer, 2011, pp. 375–376.
[38] Walsh, T.: SAT v CSP, Proceedings of the 6thInternational Conference on Principles and Practice of Constraint Programming (CP 2000), 2000,
pp. 441–456.