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

パッキング配列問題の制約モデリングと SAT 符号化
則武 治樹

番原 睦則

宋 剛秀

田村 直之

井上 克巳

制約モデリングは与えられた問題を効率よく解く上で重要な役割を果たすことが知られている．近年，大規模な命
題論理の充足可能性判定 (SAT) 問題を高速に解くことが可能な SAT ソルバーが実現され，制約充足問題 (CSP;
Constraint Satisfaction Problem) を SAT 問題に符号化して，高速な SAT ソルバーを用いて求解するアプローチ
が成功を収めている．本論文では，組合せデザイン分野の一問題であるパッキング配列 (P A) 問題を例にとり，SATに基づく制約モデリングについて考察する．P A は別名で相互直交的な部分ラテン方陣系とも呼ばれる困難な組合せ問題であり，データベースのディスク最適配置などへの応用が知られている．まず最初に，P A 問題を異なる観点から捉えた 4 つの制約モデル (CSP 表現) を提案する．次に，これらの制約モデルを順序符号化法を用いて SAT 問題に符号化する方法を示す．なかでも，基本・相違モデルは，与えられた P A のパッキング制約について，その符号化後の節数を小さく抑えられる点が特長である．最後に，組合せデザイン・ハンドブックにある P A 問題を用いて，提案する制約モデルの比較・評価を行った．実験の結果，最適値が未知であった 2 問について既知の上限が最適値であることを示し，5 問について新しい下限を得ることに成功した．

Constraint modeling is known to play an important role in solving problems eﬃciently. Remarkable improvements of SAT solvers have been made over the last decade. Such improvements encourage researchers
to solve Constraint Satisfaction Problems (CSPs) by encoding them into SAT. In this paper, we study SATbased constraint modeling of the Packing Array (P A) problem in Combinatorial Designs. P A is also called
mutually orthogonal partial latin squares and has been applied to optimal disk allocation in Databases. We
first present four constraint models from diﬀerent viewpoints of the P A problem, and then present their SAT
encodings based on the order encoding. Particularly, basic alldiﬀ model is designed to reduce the numberof clauses for the packing constraints of a given P A. To evaluate the eﬃciency of our proposed models,
we carried out experiments on the P A problems in Handbook of Combinatorial Designs. We succeeded inproving the optimality of previously known upper bounds for two arrays and in obtaining improved lower
bounds for five arrays.

thogonal Arrays) の拡張である [13]．P A は別名で相1 はじめにパッキング配列 (P A; Packing Arrays) は，組互直交的な部分ラテン方陣系 (Mutually Orthogonal
Partial Latin Squares) †1 とも呼ばれる求解困難な組

合せデザイン分野の代表的な問題である直交表 (Or-合せ問題であり，データベースのディスク最適配置などへの応用が知られている [2]．直交表のもう一つのConstraint Modeling and SAT Encoding of the Packing Array Problem
Haruki NORITAKE, 神戸大学大学院システム情報学研
究科, Graduate School of System Informatics, Kobe
University.
Mutsunori BANBARA, Takehide SOH, Naoyuki
TAMURA, 神戸大学情報基盤センター, Information
Science and Technology Center, Kobe University.
Katsumi INOUE, 国立情報学研究所情報学プリンシプル
研究系, Principles of Informatics Research Division,
National Institute of Informatics.

拡張として，カバリング配列 (CA; Covering Arrays)がある．CA はソフトウェアテストの分野に広く応用され，群論等の数学的手法，メタヒューリスティ
クス，線形計画法，制約充足問題 (CSP; Constraint

Satisfaction Problem)，命題論理の充足可能性判定†1 本 論 文 で は Mutually Orthogonal Partial Latin
Squares の 和 訳 と し て “相 互 直 交 的 な 部 分 ラ テ ン
方陣系” を用いる．

(SAT) など，これまで数多くの CA 構成手法が提案されている [4] [8] [9] [10] [11] [12] [21] [22] [23] [29] [30] [33][35] [45] [49]. これらの研究の解説論文としては [44] がある．しかしながら，P A 構成手法に対する既存研究は，グラフ理論等を用いた数学的手法 [1] [39]，メタヒューリスティクス [38]，線形計画法 [8] のみであり，

CSP および SAT を用いた手法は筆者らの知る限り

図1

SAT を用いた問題解法

存在しない．
制約モデリング [36] は，与えられた問題を効率よ

題に対して，未知の最適値を決定するなど優れた性能

く解く上で重要な役割を果たすことが知られており，主として CSP の分野で研究が進められてきた．しかを示している [4] [5] [27] [28] [37] [40]．また，順序符号化法の有効性は，SAT 型 CSP ソルバー Sugar †3 がし，近年 SAT 技術 (特に，SAT 符号化と SAT ソル

2008–2009 年国際 CSP ソルバー競技会において 2 年バー) が求解困難な問題を解くための基盤技術として連続優勝 (GLOBAL 部門) したことからも伺える．

整備され，SAT に基づく制約モデリングの重要性が

図 1 にモデリング，符号化，ソルバーの関係を示高まっている．なぜならば，与えられた問題の求解効

す．本論文では，パッキング配列を例にとり，特に順率は使用する符号化法とソルバーだけでなく，制約モ

序符号化法と CDCL ソルバーに適した制約モデリン

デリングにも大きく依存するからである．さらに，どグについて考察する (図 1 の破線部分)．

のような制約モデルが適しているかは自明ではない．

本論文ではまず最初に，P A を構成する問題に対SAT は与えられた命題論理式の充足可能性を判定して，基本行列モデル，拡張行列モデル，拡張・相する問題である．SAT は Cook により最初に NP 完

異モデル，基本・相異モデルと呼ぶ 4 つの制約モデ全性が証明された問題であり，人工知能および計算

ル (CSP 表現) を提案する．特に拡張・相異モデルは，機工学における最も基本的な問題として，論理合成，

与えられた P A のパッキング制約を CSP における代プランニング問題，スケジューリング問題，ハード

表的なグローバル制約 [47] である alldiﬀerent 制約を

ウェア検証，ソフトウェア検証，定理証明，CSP な用いて簡潔に表現できる．

ど，様々な分野に応用されている [7] [24]．

次に，これらの制約モデルを順序符号化法を用い

近年，大規模な SAT 問題を高速に解くことが可能
な SAT ソルバー [31] †2 が実現され，これらの分野へて SAT 問題に符号化する方法を示す．しかし，単純の実用的応用が急速に拡大している．特に，CSP をする符号化後の節数が大きくなる問題が生じる．実SAT 符号化 [42] した後，高速な SAT ソルバーを用際に，与えられた P A(b; k, g) に対して，基本・相異いて (元の CSP の) 解を求めるアプローチが成功をモデルを除く 3 つの制約モデルでは，パッキング制

収め，これまで数多くの SAT 符号化法が提案されて約の SAT 符号化に O(g 2 ) の節数が必要になる．これいる [6] [14] [18] [25] [26] [34] [40] [41] [43] [46] [48]．

に対して，基本・相異モデルは拡張・相異モデルのに順序符号化法を適用した場合，パッキング制約に対順序符号化法 [40] [41] は，整数有限領域上の CSP

alldiﬀerent 制約を分解することにより，符号化後の節を SAT 問題に符号化する比較的新しい SAT 符号化

数を O(g) に抑えることができる点が特長である．

法である．順序符号化法は，求解困難な問題として知最後に，提案モデルの有効性を比較・評価するためられるショップ・スケジューリング問題，二次元矩形に，2007 年に出版された組合せデザイン・ハンドブッ

パッキング問題，組合せテストのテストケース生成問

ク [13] にある最大の P A を構成する問題 (全 46 問)†2 本論文では特に断らない限り，現在高速 SAT ソルバーの主流となっている CDCL (Conflict-Driven Clause
Learning) ソルバー [31] を意味する．

を用いて実行実験を行った．その結果，提案モデルは†3 http://bach.istc.kobe-u.ac.jp/sugar/

1
0
0
0
1
1
1
2
2
2
図2

2
0
1
2
0
1
2
0
1
2

3
0
2
1
1
0
2
2
1
0

(1, 2)
0
1
2
3
4
5
6
7
8

4
0
2
1
2
1
0
1
0
2

最適な P A(9; 4, 3) の例

図3(1, 3)
0
2
1
4
3
5
8
7
6

(1, 4)
0
2
1
5
4
3
7
6
8

(2, 3)
0
5
7
1
3
8
2
4
6

(2, 4)
0
5
7
2
4
6
1
3
8

(3, 4)
0
8
4
5
1
6
7
3
2

図 2 の P A(9; 4, 3) に対する拡張行列

最適値が未知であった 2 問について既知の上限が最表 1 に組合せデザイン・ハンドブック [13] に記載され適値であることを示し，5 問について新しい下限を得ている，P AN (k, g) に対する既知の上下限を示す．表ることに成功した．さらに，与えられた P A(b; k, g)の (k, g) 成分が整数 m の場合は，P AN (k, g) = m をの kb の値に着目し，提案モデルの比較考察，対称性

表し，ℓ–u の場合は，ℓ ≤ P AN (k, g) ≤ u を表してい除去の効果について述べた．

る．k ≤ 2g の場合しか記載されていないのは，k > 2g

以降，次の節 2 では，パッキング配列の定義と関については，Adbel-Ghaﬀar らによって既に決定され連研究について述べる．提案する制約モデルを節 3ているためである [1]．なお，次の 6 つについては，で説明した後，それらの SAT 符号化を節 4 で示す．

ハンドブック出版以前に，Stardom [38] によって表 1

節 5 ではパッキング配列の対称性の除去について簡より良い結果が得られている：31 ≤ P AN (5, 6), 31 ≤

単に触れる．節 6 で提案モデルの比較・評価を行い，P AN (6, 6), 20 ≤ P AN (7, 6), 17 ≤ P AN (8, 6),

最後に節 7 で本論文をまとめる．

P AN (9, 6) = 14, P AN (11, 7) = 15.
以下，SAT を用いたアプローチをよりわかりやす2 パッキング配列と関連研究くするために，2 つの問題を定義する．P A問題とは，以下の定義は，論文 [39] に基づいている．

与えられた ⟨k, g, b⟩ に対して，P A(b; k, g) が存在す

定義 1 パッキング配列 P A(b; k, g) とは以下の条件

るかどうかを判定し，存在する場合，P A(b; k, g) をを満たす b × k 配列 A = (aij ) である．

構成する問題である．P A最適化問題とは，与えら(1) aij ∈ Zg = {0, 1, 2, . . . , g − 1}

れた ⟨k, g⟩ に対して，P AN (k, g) = b となる最大の(2) 任意の異なる 2 つの列 1 ≤ c1 < c2 ≤ k，

P A(b; k, g) を構成する問題である．

および任意の値の組 (x1 , x2 ) ∈ Zg 2 に対して，

本論文は，P A 問題に対する制約モデルおよびそx1 = arc1 かつ x2 = arc2 を満たす行 r が高々一の SAT 符号化について述べる．P A 最適化問題の解つ存在する (パッキング制約)．

は，b を変化させた複数の P A 問題を解くことによっ

定義 2 パッキ ン グ 配 列 数 P AN (k, g) と は ，て求めることができる．すなわち，SAT 符号化されP A(b; k, g) が存在する最大の b である．

た P A 問題群は，充足可能 (SAT) と充足不能 (UNSAT)

定義 3 P AN (k, g) = b の と き ，パッキ ン グ 配 列の両方の問題を含む可能性がある．最適値 (最大の b)

P A(b; k, g) は最適であるという．

は，SAT と UNSAT の境界に位置する．なお，既知の

図 2 に，最適な P A(9; 4, 3) の例を示す．最初の 22

列について，(0, 0) から (2, 2) までの全部で 3 = 9 通

上限に対する P A 問題が SAT の場合は，その上限が最適値となる．

りあるそれらの値の組合せすべてが，高々一つだけ存本研究と関連が深い研究として，Hnich らの CA

在することがわかる (ボールド体で表示)．他のどの 2問題に対する制約モデルおよびその SAT 符号化があ列の組合せについても同様の性質を満たす．

る [22] [23]．CA は，“ 高々一つ ” という P A のパッ

表1

g\k
3
4

3

4
9

5

6

6

4

16

5

7

8

9

8

5

25

15

10

既知の P AN (k, g) [13]

9

10

10

11

12

12

12

9

7

21

14–15

14

8

28
64

14

14

10

15

16 17 18

16

12

7

6 36 34 30–34 30–34 16–34 12–19 12–14
49

13

22–34 16–25 16–19 16–17

9

キング制約 (定義 1 の 2) を，“ 少なくとも一つ ” と

81

27–45 27–30

27

16

18–21 18–19 18 18 14て，1 つの行列と 1 種類の制約から構成される．

いうカバレッジ制約に置き換えたものである．Hnich• 基本行列とは，整数変数を要素にもつ b × k 行

らは，CA 問題に対して，従来の非 SAT 型 CSP ソ

列である．各要素 xr,i (1 ≤ r ≤ b，1 ≤ i ≤ k)

ルバーの利用を前提とした制約モデル，確率的 SAT

は P A の各要素を表し，そのドメインは xr,i ∈ソルバーの利用を前提とした支持符号化法 [18] [26]{0, 1, 2, . . . , g − 1} である．基本行列は P A その

ベースの CA の符号化を提案している．これに対しものを表す行列である．

• パッキング制約は以下のように表される．

て，本研究は P A 問題に対して，SAT 型 CSP ソル
バー (特に，順序符号化法と CDCL ソルバーの利用)¬(xr,i = m)∨¬(xr,j = n)に適した制約モデルを提案する点が大きく異なる．

¬(x

∨

¬(x

r ′ ,i= m)r ′ ,j

= n)

∨
(1)

Hnich らの制約モデルとの具体的な違いは，提案すただし，1 ≤ r < r ′ ≤ b, 1 ≤ i < j ≤ k, 0 ≤るモデルが alldiﬀerent 制約を使っているのに対して，m, n ≤ g − 1．

Hnich らは global cardinality 制約を使っている点で制約 (1) は，“基本行列のどの 2 つの列に対しても，2ある．global cardinality 制約は，変数に割り当てられg 通りある値の組合せすべてが高々1 つ存在する”

る値の出現回数をカウントする必要があり，一般にというパッキング制約を，基本行列上の at most one

alldiﬀerent 制約より計算コストが大きい．また，CA制約を使って定義通りに表している．この制約モ問題に対して，CDCL ソルバーと順序符号化法の組合せが，Hnich らの確率的 SAT ソルバーに適した

デルの欠点は，パッキング制約に対して生成される( )( )
at most one 制約の個数が 2b k2 g 2 と，非常に多く

SAT 符号化よりも優れた性能を示すことは，先行研なる点である．

究 [4] で確認されている．

3. 2 拡張行列モデル

3 制約モデル

拡張行列モデルでは，CSP 分野で用いられる拡張

本節では，P A 問題に対して，基本行列モデル，拡行列 [23] の概念を導入する．拡張行列モデルは，与張行列モデル，拡張・相異モデル，基本・相異モデル

えられた P A(b; k, g) に対して，2 つの行列と 2 種類と呼ぶ，4 つの新しい制約モデルを提案する．これらの制約から構成される．

の制約モデルは，CSP 分野で広く用いられる行列モ• 基本行列 (基本行列モデルと同じ)

デル [16] に基づいている．行列モデルは，変数を要( )• 拡張行列とは，整数変数を要素にもつ b × k2 行

素にもつ 1 つ以上の行列 (変数の集合) と，その行列列である．各要素 yr,(i,j) (1 ≤ r ≤ b, 1 ≤ i <

上および行列間の制約式から構成される．

j ≤ k) は基本行列の変数の組 (xr,i , xr,j ) に対応
し，そのドメインは yr,(i,j) ∈ {0, 1, 2, . . . , g 2 −1}

3. 1 基本行列モデル
基本行列モデルは，与えられた P A(b; k, g) に対しである．

• パッキング制約は以下のように表される．
()()¬ yr,(i,j) = ℓ∨ ¬ yr′ ,(i,j) = ℓ(2)′

拡張・相異モデルの特長は，“どの 2 つの列に対しても，g 2 通りある値の組合せすべてが高々1 つ存在

ただし，1 ≤ r < r ≤ b, 1 ≤ i < j ≤ k, 0 ≤する” という P A のパッキング制約が，“拡張行列のℓ ≤ g − 1．
• チャネリング制約とは，拡張行列の各変数 yr,(i,j)

各列に出現する値がすべて異なる” という制約に置き( )換えられ， k2 個の alldiﬀerent 制約によって簡潔に表と基本行列の各変数 xr,i と xr,j を関係づける制現される点である．図 3 から，拡張行列の各列に出約であり，以下のように表される．

現する値がすべて異なっていることがわかる．

2yr,(i,j) = gxr,i + xr,j(3)

ただし，1 ≤ r ≤ b, 1 ≤ i < j ≤ k ．
拡張行列モデルの特長は，“どの 2 つの列に対して
2

3. 4 基本・相異モデル
拡張・相異モデルは，基本行列モデル，拡張行列モ

も，g 通りある値の組合せすべてが高々1 つ存在す

デルと比較して，パッキング制約を alldiﬀerent 制約る” という P A のパッキング制約が，“拡張行列の各を用いて簡潔に表現することができる．しかし，SAT列について，0 から g − 1 までの値が高々1 つ存在

符号化を用いる場合，符号化後の節数が大きくなるとする” という制約に置き換えられる点である．すなわ

いう問題は依然として残る．この問題を解決するため

ち，パッキング制約は拡張列上の at most one 制約をに，拡張行列上の alldiﬀerent 制約を基本行列上の ̸=使って表される．図 3 に，図 2 の P A(9; 4, 3) に対応

制約に置き換えることにより，符号化後の節数を小さする拡張行列を示す．拡張行列の各列に 0 から 8 ま

く抑える基本・相異モデルを提案する．

2での値が高々1 つだけ存在していることがわかる．
拡張行列の導入は一見冗長に思われるが，P A 問題

基本・相異モデルは，与えられた P A(b; k, g) に対して，1 つの行列と 1 種類の制約から構成される．

に類似した CA 問題に対する有効性が実験的に示さ• 基本行列 (基本行列モデルと同じ)れている [4] [23]．この拡張行列モデルの欠点は，基• パッキング制約は以下のように表される．

本行列モデルと同様に，パッキング制約に対して生成( )( )される at most one 制約の個数が 2b k2 g 2 と非常に多くなる点である．

(xr,i ̸= xr′ ,i )∨(xr,j ̸= xr′ ,j )(5)′

ただし，1 ≤ r < r ≤ b, 1 ≤ i < j ≤ k ．
制約 (5) は，拡張・相異モデルのパッキング制約 (4)を以下のように分解することで得られる．

3. 3 拡張・相異モデル
拡張・相異モデルでは，CSP における最も代表的なグローバル制約 [47] である alldiﬀerent 制約を用い⇐⇒る．グローバル制約とは，引数として任意の数の変数⇐⇒をとり，それらの間に成り立つ関係を表現するもので()
alldiﬀerent y1,(i,j) , y2,(i,j) , . . . , yb,(i,j)∧()
yr,(i,j) ̸= yr′ ,(i,j)
1≤r<r ′ ≤b∧((xr,i ̸= xr′ ,i ) ∨ (xr,j ̸= xr′ ,j ))1≤r<r ′ ≤bある．alldiﬀerent(X1 , X2 , . . . , Xn ) は，各変数 Xi に

このように，パッキング制約を基本行列上の ̸= 制約

割り当てられる値がすべて異なることを表す制約であで表すことにより，拡張行列およびチャネリング制約

る．拡張・相異モデルは，与えられた P A(b; k, g) には不要となり，生成される節数を小さく抑えることが対して，2 つの行列と 2 種類の制約から構成される．

できる．節数に関する詳細な比較は節 4. 2 で述べる．

• 基本行列 (基本行列モデルと同じ)

最後に，これまで述べた 4 つの制約モデルについ• 拡張行列 (拡張行列モデルと同じ)て，P A のパッキング制約をどの行列上でどのような• パッキング制約は以下のように表される．
()(4)
alldiﬀerent y1,(i,j) , y2,(i,j) , . . . , yb,(i,j)

制約を使って表現するか，によって分類した表を示す

ただし，1 ≤ i < j ≤ k ．

• チャネリング制約 (拡張行列モデルと同じ)(表 2 参照)．

表2

制約モデルの分類∧∨

パッキング制約at most one 制約

alldiﬀerent 制約

bi∑n

基本行列モデル

基本・相異モデル

拡張行列

拡張行列モデル拡張・相異モデル

動くとし，変換 ()(a z ≤ b)#≡i

i=1 bi = c − n + 1 を満たすように#

基本行列

ここで bi は，

4 SAT 符号化

(ai zi ≤ bi )#は以下のように定義する．

(a > 0) p(z ≤ ⌊b/a⌋)¬p(z ≤ ⌈b/a⌉ − 1)

(a < 0)

4. 1 順序符号化法の概要

ただし，z の取り得る最小値未満の a については

順序符号化法 [40] [41] では，各整数変数 z につp(z ≤ a) を偽に変換し，最大値以上については真に変いて，そのドメインが {a1 , a2 , . . . , an } の時 (ただし換する．例えば，整数変数 w, z のドメインが {0, 1, 2}

a1 < a2 < . . . < an )，z ≤ ai を表す n − 1 個の命の時，制約 w − z ≤ −1 は以下の 3 つの節に符号化さ

題変数 p(z ≤ a1 ), p(z ≤ a2 ), . . . , p(z ≤ an−1 ) を用れる．

いる．なお，z ≤ an は常に真であるため，命題変数¬p(z ≤ 0)p(w ≤ 0) ∨ ¬p(z ≤ 1)p(w ≤ 1)p(z ≤ an ) は不要である．また，これらの命題変数間

ここで，p(w ≤ 0) ∨ ¬p(z ≤ 1) は，「w ≤ 0 またはの関係を表す以下の節を用いる．

z > 1」であること，すなわち「w ≥ 1 かつ z ≤ 1」¬p(z ≤ ai ) ∨ p(z ≤ ai+1 )(1 ≤ i ≤ n − 2)

が制約に違反する領域であることを表している．

例えば，変数 z のドメインが {0, 1, 2} の場合，2 つのw ̸= z の場合，一旦 w − z ≤ −1 ∨ z − w ≤ −1 の命題変数 p(z ≤ 0), p(z ≤ 1) を用い，以下の節を追ように線形制約に置き換え，さらに Tseitin 変換を用加する．

いて (p ∨ q) ∧ (¬p ∨ w − z ≤ −1) ∧ (¬q ∨ z − w ≤ −1)¬p(z ≤ 0) ∨ p(z ≤ 1)と変換してから符号化する (p，q は新しい命題変数)．

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

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

は 3 通りあり，それぞれ z = 0, z = 1, z = 2 に対応¬p ∨ ¬p(z ≤ 0)

する．

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

解釈

¬p ∨ p(w ≤ 1)

1

1

z=0

¬q ∨ ¬p(w ≤ 0)

0

1

z=1

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

0

0

z=2

¬q ∨ p(z ≤ 1)

制約については，制約に違反する範囲を符号化す

4. 2 P A問題の順序符号化

る．例えば，整数変数 w，z のドメインが {0, 1, 2} の節 3 で提案した 4 つの制約モデルを，順序符号化場合，算術比較 w ≤ z は以下の 2 つの節に符号化さ法を用いて SAT に符号化する方法を述べる．基本行
列の整数変数 xr,i ，拡張行列の整数変数 yr,(i,j) ，拡張

れる．

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

線形式を用いた線形制約については，より簡潔な符号化が可能である．今，ai を非零の整数定数，c を整数定数，zi を互いに異なる整数変数とする．この時，∑
制約 ni=1 ai zi ≤ c は以下のように符号化できる．

行列のチャネリング制約 (3) については，節 4. 1 で述べたように符号化される．よって以下では，各制
約モデルのパッキング制約の SAT 符号化について述べる．
基本行列モデル: パッキング制約 (1) は，以下のように符号化される．

表3

P A(b; k, g) 問題に対する SAT 符号化後の節数の比較

基本行列モデル

拡張行列モデル拡張・相異モデル

基本・相異モデル

基本行列

bk(g − 1)

パッキング制約–(b)(k) 2g
2 2

チャネリング制約–

bk(g − 1)(k) 2
b 2 (g − 1)(b)(k) 2(2g + 1)2 2
( 2 2)
O bk gbk(g − 1)

拡張行列bk(g − 1)(k) 2
b 2 (g − 1)(b)(k) 2g
2 2( 2 2)
O bk g–(b)(k)
2

2(4g + 3)–

後，各等号否定 xr,i ̸= xr′ ,i は，節 4. 1 で述べた

p(xr,i ≤ m − 1)∨¬p(xr,i ≤ m)∨p(xr,j ≤ n − 1)∨¬p(xr,j ≤ n)∨

表 3 に各制約モデルについて，SAT 符号化後の節

p(xr′ ,i ≤ m − 1)∨¬p(xr′ ,i ≤ m)∨

数を示す．与えられた P A(b; k, g) に対して，基本・p(xr′ ,j ≤ n − 1)∨¬p(xr′ ,j ≤ n)

た だ し ，1 ≤ r < r ′ ≤ b, 1 ≤ i < j ≤制約の符号化に O(g 2 ) の節数が必要になる．これにk, 0 ≤ m, n ≤ g − 1．また，p(xr,i ≤ −1) と対して，基本・相異モデルは符号化後の節数を O(g)p(xr′ ,j ≤ −1) は偽とする．例えば，最初の 2 行に抑えることができる．

ように符号化される．

相異モデルを除く 3 つの制約モデルでは，パッキングは ¬(xr,i = m) ∨ ¬(xr,j = n) を表している．

SAT 符号化の良し悪しについては，利用する SAT

拡張行列モデル: パッキング制約 (2) は，以下のソルバーの特性 (CDCL ソルバーか確率的ソルバー
か) によって異なるため明確な基準はないが，SAT 符

ように符号化される．

p(yr,(i,j) ≤ ℓ − 1)p(yr′ ,(i,j) ≤ ℓ − 1)∨¬p(yr,(i,j) ≤ ℓ)∨¬p(yr′ ,(i,j) ≤ ℓ)∨′

た だ し ，1 ≤ r < r ≤ b, 1 ≤ i < j ≤号化の研究者の間では以下の 2 つの基準がよく用いられる：(a) 符号化後の SAT 問題に対する SAT ソル
バーの単位伝播と元の CSP に対する制約伝播との関

2k, 0 ≤ ℓ ≤ g − 1．また，p(yr,(i,j) ≤ −1) と連，(b) 符号化後の節数 (少ない方が良いとされる)．

p(yr′ ,(i,j) ≤ −1) は偽とする．

(a) について，本論文で用いた順序符号化法は，SAT

拡張・相異モデル: パッキング制約 (4) についてソルバーの単位伝播が元の CSP に対する範囲伝播

は，まず alldiﬀerent 制約を以下のように分解する．
()
alldiﬀerent y1,(i,j) , y2,(i,j) , . . . , yb,(i,j)∧()⇐⇒
yr,(i,j) ̸= yr′ ,(i,j)に対応しており，効率の良い求解が可能である [42]．

1≤r<r ′ ≤b(b) については，表 3 に示すように，基本・相異モデ
ルの節数が最も少なく，他のモデルよりも優れていると言える．

ただし，1 ≤ i < j ≤ k ．その後，各等号否定

yr,(i,j) ̸= yr′ ,(i,j) は，節 4. 1 で述べたように符号5 対称性の除去

化される．

パッキング配列は対称性が高く，対称解が多く存在

基本・相異モデル: パッキング制約 (5) について
は，新しい命題変数 p, q を導入し，まず以下のよとが知られている [39]．

• 行と列に関する対称性

うに置き換える．

(xr,i ̸= xr′ ,i ) ∨ (xr,j ̸= xr′ ,j )⇐⇒する．パッキング配列には以下の対称性が存在するこ与えられたパッキング配列に対して，任意の相(p ∨ q)∧異なる 2 つの行 (あるいは列) を入れ替えたも(¬p ∨ (xr,i ̸= xr′ ,i ))∧のも解となる．例えば，図 4 は図 2 に挙げた(¬q ∨ (xr,j ̸= xr′ ,j ))ただし，1 ≤ r < r ′ ≤ b, 1 ≤ i < j ≤ k ．そのP A(9; 4, 3) の 1 列目と 2 列目を入れ替えることで得られる対称解である．

• 値に関する対称性

1
0
1
2
0
1
2
0
1
2

与えられたパッキング配列に対して，任意の列中の値をスワップしたものも解となる．例えば，
図 5 は図 2 に挙げた P A(9; 4, 3) の 1 列目の値を(0 を 2, 1 を 0, 2 を 1 に) スワップすることで得られる対称解である．

CSP 分野において，対称解を除去することは対称性除去 (Symmetry Breaking) と呼ばれ，重要な研究課題となっている [19]．一般に対称性除去は解探

図4

2
0
0
0
1
1
1
2
2
2

3
0
2
1
1
0
2
2
1
0

4
0
2
1
2
1
0
1
0
2

列に関する対称解

1
2
2
2
0
0
0
1
1
1
図5

2
0
1
2
0
1
2
0
1
2

3
0
2
1
1
0
2
2
1
0

4
0
2
1
2
1
0
1
0
2

値に関する対称解索のコストを減らす効果がある．
行と列に関する対称性を除去するためには，以下のベンチマーク問題 (79 問)： 各 P AN (k, g) の既

2 つの手法のいずれかを用いる．なお，これらは同時知の下限 ℓ および上限 u に対して，b を ℓ ≤ b ≤に使用することはできない．

min(ℓ + 5, u) のように変化させた P A(b; k, g) 問

• Double Lex [16]：基本行列の連続する相異な

題全 79 問．既知の下限 ℓ は筆者らの先行研究 [32]

る 2 つの行，および連続する相異なる 2 つの列で得られた値を反映した値である．既知の上限 uに対して辞書式順序制約 (Lexicographic Orderは表 1 と同じである．b の上限を min(ℓ + 5, u)Constraint) を適用する．

に制限しているのは，既知の上限 u は Plotkin• Snake Lex [20]：Double Lex の改良として提案

bounds と呼ばれる符号理論の定理 [39] より得らされたスネーク順序 (Snake Ordering) に基づく

れた弱い上限であり，ℓ + 5 を超える大きな b を対称性除去手法である．釣合い型不完備ブロック

もつ P A 問題は現実的な時間内では解けないこ計画などに対する有効性が示されている．

とが先行研究 [32] で確認されているためである．

値に関する対称性を除去するためには，与えられた

次に，上記ベンチマーク問題 (P A 問題，79 問) に

P A(b; k, g) に対して，新しく整数変数 fi,v (1 ≤ i ≤対して，制約モデル (4 通り)，対称性除去の有無 (3k, 0 ≤ v ≤ g − 1) を導入する．fi,v は列 i に出現す通り) の計 4 × 3 = 12 通りの CSP 表現を生成した．

る値 v の個数を表す．その上で，すべての列 i に対し制約モデル (4 通り)： 基本行列モデル，拡張行て制約 fi,0 ≤ fi,1 ≤ · · · ≤ fi,g−1 を適用する．以下，

列モデル，拡張・相異モデル，基本・相異モデル

この制約を出現個数制約と呼ぶ．なお，出現個数制約の 4 つの制約モデル．

は Double Lex および Snake Lex のいずれかと同時対称性除去の有無 (3 通り)： Double Lex と出現に使用することができる．これらの手法はパッキング

個数制約の組合せ (以降，“D” で表示)，Snake

配列の対称解を除去するものであり，解の存在性は保Lex と出現個数制約の組合せ (“S” で表示)，対たれる．

称性除去なし (“無” で表示) の 3 通り．
以降，これら 12 通りの組合せを，“制約モデル名

6 実行実験(SB)”，SB ∈ {D, S, 無 } で表す．例えば，基本行列

提案する制約モデルの有効性を比較・評価するため

モデル (D) は，基本行列モデルに Double Lex と出に，組合せデザイン・ハンドブック [13] にある P A 最適化問題 (全 46 問，表 1 参照) の最適値 P AN (k, g)を求める実験を行った．

現個数制約を適用したモデルを表す．
最後に，ベンチマーク問題 (79 問) に対して，上記の組合せ (12 通り) を用いて生成された計 79 × 12 = 948
通りの CSP 表現を，順序符号化法を用いて SAT に

6. 1 実験概要

符号化し，以下の 3 種類の SAT ソルバーを用いて求実験に用いたベンチマーク問題は以下の通りである．

解した．順序符号化を行うプログラムには，SAT 型

表4
基本行列モデル

k g b

無

D

ベンチマーク結果：CPU 時間 (秒)拡張行列モデル

無

S

D

S

拡張・相異モデル

基本・相異モデル

無

無

D

S

D

S

4 3 9∗<0.00 <0.00 <0.00 <0.00<0.00 <0.00 <0.00 <0.00 <0.00 <0.00 <0.00 <0.00

5 3 6∗<0.00 <0.00<0.00

6 3 4∗<0.00 <0.00 <0.00 <0.00

0.01 <0.00

5 4 16∗0.01

6 4 9∗

0.03

0.20

0.03

0.05

7 4 8∗

5.12

96.72

0.33

37.83

<0.00 <0.00 <0.00 <0.00

8 4 5∗
6 5 25∗0.04

7 5 15∗6.46

8 5 10∗0.05

9 5 10∗T.O

10 5 7∗3 6 36∗

0.01

0.22

0.02

0.01

0.01

0.01 <0.00

0.01

0.01 <0.00 <0.00<0.00 <0.00 <0.00 <0.00 <0.00 <0.00 <0.00 <0.00
0.02

0.02

0.02

0.03

0.07

0.09

0.04

0.02

0.66

0.23

0.62

1.47

0.09

7.41

1.16

0.02

88.74

0.05

0.27

T.O

T.O

0.41

0.18

2.34

0.01

0.01

0.17

0.01

0.01 <0.00 <0.00 <0.00

0.08

0.13

0.48

0.14

15.80

0.03

0.16

0.44

T.O

70.95

T.O

17.35

0.08

T.O

T.O

T.O

15.27

T.O

T.O

62.62

31.54

0.07

3.02

0.03

0.07 477.43

1.89 1309.21 1399.11

0.31

0.06

0.11

14.93

T.O

T.O

T.O

T.O

27.56

5.83

1.09

0.93

0.02

0.46

0.02

0.03

0.16

0.05 401.60

0.03

5.96

0.06

0.04

0.04

0.03

0.10

0.07

0.10

0.10

0.07

0.05

0.11

0.10

0.02

0.07

0.05

4 6 34∗

T.O

0.36

4.22

T.O

1.95

4.55 471.42

3.12

1.86

1.23

26.41

31.54

5 6 31

T.O

T.O 185.56

T.O

T.O 951.94

T.O

T.O 625.76 3500.12

6 6 31

T.O

T.O

T.O

T.O

T.O

T.O

T.O

20.50

T.O

T.O

T.O

T.O

8 6 17

24.35

T.O

T.O

17.42

T.O

T.O 243.48

T.O

T.O

T.O

T.O

T.O

9 6 14∗

0.93

T.O

T.O

10.17

T.O

T.O

20.99

T.O

T.O

26.77

T.O

T.O

10 6 12∗

0.07

T.O

0.13

0.11

0.45

9.35

2.87

30.09

0.68

0.36

0.28

0.32

11 6 12∗

T.O

T.O

T.O

T.O

T.O

T.O

T.O

3.21

T.O 2209.84

0.35

5.90

12 6 9∗

T.O

T.O

T.O

T.O

T.O

T.O

T.O

T.O

T.O

0.36

0.57

8 7 49∗

T.O

T.O

T.O

T.O 2440.90

T.O

T.O

T.O

T.O

T.O

T.O

T.O

11 7 15∗

1.96 142.95

17.99

9.05

181.68 369.41

1.59

34.88 449.68

3.62

25.22

17.81

116.62 209.01

T.O 592.72

0.14

12 7 14∗ 2382.49

2.45

37.97 462.93

9.39

T.O 114.61 405.01

0.17

0.27

13 7 14∗

T.O

16.66

T.O

T.O

T.O 989.76

T.O

T.O

T.O

T.O

2.50

0.96

14 7 10∗6.90 1632.34

0.17

3.55

0.14

0.24

T.O

1.23

0.66

4.99

0.65

0.05

0.46

0.34

10 8 25 1058.90

T.O

T.O 791.83

T.O

T.O 2048.01

T.O

T.O

T.O

T.O

T.O

11 8 21

14.07

T.O

T.O

6.62

T.O

T.O 104.01

T.O

T.O

T.O

T.O

T.O

11 8 22781.94

T.O

T.O

T.O

T.O

T.O 1013.51

T.O

T.O

T.O

T.O

T.O

12 8 18

8.73

T.O

T.O

14.69

T.O

T.O

44.59

T.O

T.O

50.07 3467.89 2283.27

12 8 19∗

T.O

T.O

T.O 562.61

T.O

T.O

T.O

T.O

T.O

T.O

T.O

13 8 17∗

T.O

T.O 218.30 134.17

T.O

T.O 2536.77

T.O

T.O

T.O

T.O 1802.67

14 8 16∗

T.O

30.94

9.97

T.O 223.42 160.32

T.O

6.10

2.49

15 8 16∗

52.43

T.O

28.96

T.O

T.O

T.O

T.O

T.O

880.94

T.O

T.O

T.O

T.O

T.O

8.81

7.66

16 8 12∗ 1404.82

T.O

17.75 2657.45

297.48T.O 1265.67

T.O

T.O

0.18

8.57

0.29

11 9 28

30.01

T.O

T.O

17.42

T.O

T.O

79.05

T.O

T.O

T.O

T.O

T.O

11 9 29

56.26

T.O

T.O 392.92

T.O

T.O

T.O

T.O

T.O

T.O

T.O

T.O

14 9 20

T.O

T.O

T.O 1815.91

T.O

T.O 670.59

T.O

T.O

T.O

T.O

T.O

15 9 18

T.O

7.30

21.44

T.O

106.00

24.97

T.O

18.74

25.49

50.68

10.83

8.83

16 9 18∗

T.O 318.82 221.87

T.O

324.66

T.O

T.O 585.65 2773.84

T.O

39.60

19.79

17 9 18∗

T.O 3339.23

T.O

T.O

T.O

T.O

T.O

T.O

T.O

T.O

99.14 386.88

18 9 14∗

T.O

T.O

T.O

T.O

T.O

T.O

T.O

T.O

T.O

7.27 828.76 2057.81

合計

25

21

22

26

22

20

28

20

19

25

30

31

4000
基本・相異(S)
基本・相異(D)
拡張・相異(無)拡張行列(無)基本・相異(無)基本行列(無)基本行列(S)
拡張行列(D)
基本行列(D)
拡張行列(S)
拡張・相異(D)
拡張・相異(S)3500

CPU時間(秒)

3000
2500
2000
1500
1000
500
0
0

5

10

15

20

25

30

35

解けた問題数図6

表 4 のカクタスプロット

CSP ソルバー Sugar を使用した．
SAT ソルバー (3 種類)： glucose 2.0 [3], Min-

解けた問題の合計数を示している．なお，表 4 中のP A 問題はすべて SAT であった．

iSat 2.2.0 (core) [15], clasp 2.0.4 [17] の 3 種類

解けた問題数については，基本・相異モデル (S)の CDCL ソルバー．glucose と clasp は SAT 競

が全 79 問中最多の 31 問を，次いで基本・相異モデ技会 2011 および SAT チャレンジ 2012 と呼ばれ

ル (D) が 30 問，拡張・相異モデル (無) が 28 問，拡る SAT ソルバー競技会の優勝ソルバー．

張行列モデル (無) が 26 問，基本行列モデル (無) がSAT ソルバーの CPU 時間は，Mac OS X (Xeon

25 問を解いており，基本・相異モデルが優れた性能

2.66GHz，24GB メモリ) 上で計測し，各ベンチマーを示していることがわかる．また，対称性の除去は基ク問題に対する SAT ソルバーのタイムアウト時間

本・相異モデルに対して効果があるが，他のモデルに(T.O) は 3600 秒とした．

おいては逆に解ける問題数が減る結果となった．

CPU 時間を比較するために，図 6 に表 4 のカクタ
6. 2 実験結果

スプロットを示す．横軸は解けた問題数を，縦軸は昇

表 4 に，制約モデルと対称性除去の組合せ 12 通り

順に並び替えた SAT ソルバーの CPU 時間を示してのいずれかで解けた問題 (42 問) について，求解に要いる．すなわち，この表はグラフが右にあるほど多くした glucose の CPU 時間を示す．3 つのソルバーのの問題を解き，下にあるほど高速に求解していること

うち，glucose の結果を示した理由は，glucose が全を示す．図 6 より，基本・相異モデル (S) と基本・相79 問中最多の 42 問を解き，clasp のみで解けた 1 問

異モデル (D) が，他と比較して，高速に問題を解いを除いて，MiniSat が解いた 41 問，clasp が解いた 34ていることがわかる．また，この 2 つを比較すると，問をすべて含んでいるからである．3 列目の b の値に2,200 秒付近までは基本・相異モデル (D) が良いが，“∗” が付いている場合は，その値が最適値であること

それを超えると，基本・相異モデル (S) が逆転していを示している．各問題の一番良い CPU 時間をボー

ることがわかる．

ルド体で記している．また，最後の行は，各モデルで以上，ベンチマーク問題全 79 問に関する評価では，

表5

表6

新しい結果

これまでの結果 [13] [38]20 ≤ P AN (7, 6)
22 ≤ P AN (10, 8)
16 ≤ P AN (11, 8)
16 ≤ P AN (12, 8) ≤ 19
16 ≤ P AN (13, 8) ≤ 17
27 ≤ P AN (11, 9)
18 ≤ P AN (14, 9)

新しく得られた結果
23 ≤ P AN (7, 6)
25 ≤ P AN (10, 8)
22 ≤ P AN (11, 8)
P AN (12, 8) = 19
P AN (13, 8) = 17
29 ≤ P AN (11, 9)
20 ≤ P AN (14, 9)

基本・相異モデルと基本行列モデルの比較
基本行列モデル

基本・相異モデル
無

D

範囲

問題数

無

k
≤ 0.7
b
k
> 0.7
b

56

14

6

7

9

9

9

23

11

15

15

16 21

22

合計

79

25

21

22

25 30

31

D

S

S

6. 4 考察
解けた問題数，求解に要した CPU 時間ともに，基与えられた P A(b; k, g) に対して，その縦横比 kb

本・相異モデルと対称性除去の組合せが最も効果的でを考える．すなわち， kb < 1 であれば，与えられたあった．この結果は，節 4. 2 で述べた節数の比較 (図P A(b; k, g) は縦長， kb > 1 であれば横長である．本

3 参照) に関する評価結果とも一致している．

節では，この kb の値が各制約モデルの求解性能に関係しているのではないかという仮説を基に，基本・相

6. 3 新しく得られた結果

異モデルと基本行列モデルについて比較考察を行う．

表 5 に，今回の実験で新しく得られた結果を示す．

図 7 は，横軸が昇順に並び替えた kb の値，縦軸がこれら 7 問の内訳は，これまで最適値が未知であった

解けた問題の累積数を表している．図より， kb = 0.9問題に対して，既知の上限が最適値であることを新し付近で 2 つのモデルの累積求解数が逆転し，最終的にく決定した 2 問と，新しい下限を見つけることに成

基本・相異モデル (S) が 31 問，基本行列モデル (無)功した 5 問である．例えば，P AN (12, 8) の既知の上が 25 問を解いていることがわかる．また， kb = 0.7

下限は，表 1 より 16 ≤ P AN (12, 8) ≤ 19 であった．

付近から，基本・相異モデル (S) の求解性能が右上がしかし，表 4 から P A(19; 12, 8) は SAT であるため，りに向上している点が特徴的である．
表 6 は，解けた問題数を kb = 0.7 の前後で 2 つにP AN (12, 8) = 19 であることが決定できた．
これら 7 問を求めた制約モデルの内訳は，基本行列

分けて示したものである． kb ≤ 0.7 では，基本行列モ

モデル (無) が 7 問，拡張行列モデル (無) と拡張・相デル (無) が最も多い 14 問を解き， kb > 0.7 では，基異モデル (無) が各 5 問，基本行列モデル (S)，基本・本・相異モデル (S) が最も多い 22 問を解いている．

相異モデル (無)，基本・相異モデル (S)，基本・相異

このように， kb = 0.7 の前後で，2 つのモデルの求解モデル (D) が各 1 問となっている．また，SAT ソル

性能に大きな違いがあることが確認できた．

バーは glucose と MiniSat が比較的良いものの，7 問

この kb を指標に用いた定量的な観察結果を基に，全てを解くソルバーはない．例えば，P A(23; 7, 6) は新しく得られた結果 (表 5 の 7 問) を見ると，全ての基本行列モデル (無) と clasp の組合せのみが求解にモデルで解けた P A(17; 13, 8) を除いて，それらの kb

成功している．

の値は 0.7 以下であり，基本行列モデル (無) が得意

以上，新しく得られた結果に関する評価では，基本行列モデル (無) が他のモデルより良い結果を示してとする問題であった． kb = 0.7 の定性的な意味に関する考察は，今後の重要な課題である．
最 後 に ，対 称 性 除 去 の 効 果 に つ い て 考 察 す る ．

いる．しかし，この結果は，前節で述べたベンチマー
ク問題全 79 問に関する結果とは大きく異なるものとkb

なった．次節では，“何故このような違いが生じたのており効果が認められる． kb ≤ 0.7 の場合，基本行列

か” ついて，より深く考察を行う．

モデルで求解数が減っている原因としては，値に関> 0.7 では，どちらのモデルでも求解数が増えする対称性を除去する制約の SAT 符号化に O(b2 kg)の節数が必要となり，b の大きな縦長の P A に対して符号化後の節数増大をまねく点が挙げられる．

35
基本・相異(S)
基本行列(無)30解けた問題数

25

20

15

10

5

0
0

0.2

0.4

0.6

0.8

1

1.2

1.4

1.6

k/b
図7

基本・相異モデル (S) と基本行列モデル (無) の比較

分野のモデリング技法である行列モデル [16] とグロー

7 まとめ

バル制約 [47] の効果的な利用に基づいている．その上

本論文では，組合せデザイン分野の P A 問題を取に，符号化後の節数を小さく抑える等の CSP を SAT

り上げ，順序符号化法と CDCL ソルバーに適した制で効率よく解くための工夫を加えることにより，P A

約モデリングについて考察を行った．提案した 4 つ問題に対して優れた結果を得ることができた．よっの制約モデルのうち，特に，基本・相異モデルは，与て，本論文のアプローチは，これまで CSP 分野で研えられた P A のパッキング制約について，符号化後

究および蓄積されてきた様々な組合せ問題・組合せ最の節数を小さく抑えることができる点が特長である．

適化問題のモデリングに対して適用可能であると考提案モデルの有効性を比較・評価するために，組合えられる．

せデザイン・ハンドブック [13] にある P A 最適化問
題 (全 46 問) を用いて実行実験を行った結果，最適値

参 考 文 献がこれまで未知であった 2 問について，既知の上限が[ 1 ] Abdel-Ghaﬀar, K. A. S.: On the number of mutually orthogonal partial latin squares, Ars Combinatoria, Vol. 42(1996), pp. 259–286.
[ 2 ] Abdel-Ghaﬀar, K. A. S. and Abbadi, A. E.: Optimal Disk Allocation for Partial Match Queries,
ACM Transactions on Database Systems, Vol. 18,
No. 1(1993), pp. 132–156.
[ 3 ] Audemard, G. and Simon, L.: Predicting Learnt
Clauses Quality in Modern SAT Solvers, Proceedings of the 21st International Joint Conference on
Artificial Intelligence (IJCAI 2009), 2009, pp. 399–
404.
[ 4 ] Banbara, M., Matsunaka, H., Tamura, N., andInoue, K.: Generating Combinatorial Test Cases byEﬃcient SAT Encodings Suitable for CDCL SAT

最適値であることを示し，5 問について新しい下限を得ることに成功した．与えられた P A(b; k, g) の kb の値を指標に用いて，提案モデルの比較考察を行った．
その結果，新しい結果が得られた 7 問については，全てのモデルで解けた 1 問を除いて， kb ≤ 0.7 であり，基本行列モデル (無) が得意とする問題であった．また， kb > 0.7 の問題については，基本・相異モデルと対称性除去の組合せが最も効果的であることが確認できた．
本論文で提案した制約モデルの基本部分は，CSP

Solvers, Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-17), 2010, pp. 112–
126.
[ 5 ] 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.
[ 6 ] 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.
[ 7 ] 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.
[ 8 ] Bulutoglu, D. and Margot, F.: Classification of orthogonal arrays by integer programming, Journal of Statistical Planning and Inference,Vol. 138(2008), pp. 654–666.
[ 9 ] Chateauneuf, M. A. and Kreher, D. L.: On theState of Strength-Three Covering Arrays, Journalof Combinatorial Designs, Vol. 10, No. 4(2002),
pp. 217–238.
[10] Cohen, D. M., Dalal, S. R., Fredman, M. L.,
and Patton, G. C.: The AETG System: An Approach to Testing Based on Combinatiorial Design, IEEE Transactions on Software Engineering,Vol. 23, No. 7(1997), pp. 437–444.
[11] Cohen, M. B., Dwyer, M. B., and Shi, J.:
Constructing Interaction Test Suites for HighlyConfigurable Systems in the Presence of Constraints: A Greedy Approach, IEEE Trans. Software Eng., Vol. 34, No. 5(2008), pp. 633–650.
[12] Cohen, M. B., Gibbons, P. B., Mugridge, W. B.,
and Colbourn, C. J.: Constructing Test Suites
for Interaction Testing, Proceedings of the 25th
International Conference on Software Engineering(ICSE 2003), 2003, pp. 38–48.
[13] Colbourn, C. J. and Dinitz, J. H.: Handbookof Combinatorial Designs, Chapman & Hall/CRC,
2007.
[14] 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.
[15] Eén, N. and Sörensson, N.: An Extensible SATsolver, Proceedings of the 6th International Conference on Theory and Applications of Satisfiability
Testing (SAT 2003), LNCS 2919, 2003, pp. 502–
518.
[16] Flener, P., Frisch, A. M., Hnich, B., Kiziltan,
Z., Miguel, I., Pearson, J., and Walsh, T.: Break-ing Row and Column Symmetries in Matrix Models,
Proceedings of the 8th International Joint Conference on Principles and Practice of Constraint Programming (CP 2002), LNCS 2470, 2002, pp. 462–
476.
[17] 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), MIT
Press, 2007, pp. 386–392.
[18] Gent, I. P.: Arc Consistency in SAT, Proceedings of the 15th European Conference on Artificial
Intelligence (ECAI 2002), 2002, pp. 121–125.
[19] Gent, I. P., Petrie, K. E., and Puget, J.-F.:
Symmetry in Constraint Programming, Handbookof Constraint Programming, Rossi, F., van Beek, P.,
and Walsh, T.(eds.), Elsevier, 2006, pp. 329–376.
[20] Grayland, A., Miguel, I., and Roney-Dougal,
C. M.: Snake Lex: An Alternative to Double Lex,
Proceedings of the 15th International Joint Conference on Principles and Practice of Constraint Programming (CP 2009), LNCS 5732, 2009, pp. 391–
399.
[21] Hartman, A. and Raskin, L.: Problems and Algorithms for Covering Arrays, Discrete Mathematics, Vol. 284, No. 1-3(2004), pp. 149–156.
[22] Hnich, B., Prestwich, S. D., and Selensky, E.:
Constraint-Based Approaches to the Covering Test
Problem, Proceedings of the International Workshop on Constraint Solving and Constraint Logic
Programming (CSCLP 2004), LNCS 3419, 2004,
pp. 172–186.
[23] Hnich, B., Prestwich, S. D., Selensky, E., andSmith, B. M.: Constraint Models for the Covering
Test Problem, Constraints, Vol. 11, No. 2-3(2006),
pp. 199–219.
[24] 井上克巳, 田村直之: SAT ソルバーの基礎, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 57–67.
[25] Iwama, K. and Miyazaki, S.: SAT-Variable
Complexity of Hard Combinatorial Problems,Proceedings of the IFIP 13th World Computer
Congress, 1994, pp. 253–258.
[26] Kasif, S.: On the Parallel Complexity of Discrete
Relaxation in Constraint Satisfaction Networks, Artificial Intelligence, Vol. 45, No. 3(1990), pp. 275–
286.
[27] 越村三幸, 鍋島英知, 藤田博, 長谷川隆三: SAT 変換
による未解決ジョブショップスケジューリング問題への挑戦, スケジューリング・シンポジウム 2009 講演論文集, 2009, pp. 209–213.
[28] 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.
[29] Lei, Y. and Tai, K.-C.: In-Parameter-Order:
A Test Generation Strategy for Pairwise Testing,
Proceedings of 3rd IEEE International Symposium

on High-Assurance Systems Engineering (HASE
1998), 1998, pp. 254–261.
[30] Meagher, K. and Stevens, B.: Group Construction of Covering Arrays, Journal of Combinatorial
Designs, Vol. 13, No. 1(2005), pp. 70–77.
[31] 鍋島英知, 宋剛秀: 高速 SAT ソルバーの原理, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 68–76.
[32] 則武治樹, 番原睦則, 田村直之, 井上克巳: 制約充足問題の SAT 符号化を用いたパッキング配列の構成,
2012 年度人 工知能学会全 国大会 (第 26 回) 論 文集
1E3-OS-4-1, 人工知能学会, 2012.
[33] Nurmela, K. J.: Upper Bounds for Covering Arrays by Tabu Search, Discrete Applied Mathematics, Vol. 138, No. 1-2(2004), pp. 143–152.
[34] 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.
[35] Shiba, T., Tsuchiya, T., and Kikuno, T.: Using
Artificial Life Techniques to Generate Test Cases for
Combinatorial Testing, Proceedings of 28th International Computer Software and Applications Conference (COMPSAC 2004), 2004, pp. 72–77.
[36] Smith, B. M.: Modelling, Handbook of Constraint Programming, Rossi, F., van Beek, P., andWalsh, T.(eds.), Elsevier, 2006, pp. 377–406.
[37] 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.
[38] Stardom, J.: Metaheuristics and the Search for
Covering and Packing Arrays, Master’s thesis, Simon Fraser University, Burnaby, Canada, 2001.
[39] Stevens, B. and Mendelsohn, E.: Packing
arrays, Theoretical Computer Science, Vol. 321,
No. 1(2004), pp. 125–148.
[40] 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.
[41] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Constraints, Vol. 14, No. 2(2009), pp. 254–272.
[42] 田村直之, 丹生智也, 番原睦則: 制約最適化問題とSAT 符号化, 人工知能学会誌, Vol. 25, No. 1(2010),
pp. 77–85.
[43] Tanjo, T., Tamura, N., and Banbara, M.: A
Compact and Eﬃcient SAT-Encoding of Finite Domain CSP, Proceedings of the 14th International
Conference on Theory and Applications of Satisfiability Testing (SAT 2011), LNCS 6695, Sakallah,
K. A. and Simon, L.(eds.), Springer, 2011, pp. 375–
376.
[44] 土屋達弘, 菊野亨: ペアワイズテスト - ソフトウェ
アテストの効率化を求めて -, 電子情報通信学会論文誌
D, Vol. J90-D, No. 10(2007), pp. 2663–2674.
[45] Tung, Y.-W. and Aldiwan, W. S.: Automating Test Case Generation for the New Generation Mission Software System, Proceedings of IEEE
Aerospace Conference, 2000, pp. 431–437.
[46] Van Gelder, A.: Another Look at Graph Coloring via Propositional Satisfiability, Discrete Applied
Mathematics, Vol. 156, No. 2(2008), pp. 230–243.
[47] van Hoeve, W. J. and Katriel, I.: Global
Constraints, Handbook of Constraint Programming,
Rossi, F., van Beek, P., and Walsh, T.(eds.), Elsevier, 2006, pp. 169–208.
[48] Walsh, T.: SAT v CSP, Proceedings of the 6thInternational Conference on Principles and Practice of Constraint Programming (CP 2000), 2000,
pp. 441–456.
[49] Williams, A. W.: Determination of Test Configurations for Pair-Wise Interaction Coverage,
Proceedings of 13th International Conference on
Testing Communicating Systems (TestCom 2000),
2000, pp. 59–74.