SAT - 基盤(S)離散構造処理系プロジェクト

Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
SAT 技術を用いた
組合せテストケース生成
番原 睦則
Web
神戸大学情報基盤センター
共同研究者
田村 直之 (神戸大学)
宋 剛秀 (神戸大学)
Web
Web
井上 克巳 (国立情報学研究所)
鍋島 英知 (山梨大学)
Web
Web
湊離散構造処理系プロジェクト ERATO セミナー
関西サテライトラボ 2012 年 7 月 6 日 (金)
1 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
Knuth 先生@SAT 国際会議 2012
Web
招待講演：Satisfiability and The Art of Computer Programming
問題： Colored N-Queen (N = 5)
SAT 符号化法：対数，多値
SAT ソルバー：Knuth 先生の自作
Knuth 先生の SAT2012 招待講演スライドからの抜粋
Sugar で解いてみた (by 田村先生)
N
SAT/UNSAT の別
O.E. + PHP +
Glucose(simp)
5
SAT
√
6
UNSAT
√
7
SAT
√
8
UNSAT
√
9
?
10
?
11
SAT
√
12
SAT
13
SAT
√
2 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
概要 履歴 事例
SAT 型制約ソルバー Sugar
[田村ほか,2006
Web
]
Sugar は，制約充足問題 (CSP) を命題論理式に符号化し，
SAT ソルバーを用いて求解を行う SAT 型の制約ソルバー
符号化
CSP
SAT
SAT ソルバー
CSP の解
•
•
•
•
復号化
SAT の解
順序符号化法 [田村ほか,2006] と呼ばれる SAT 符号化法を使用．
制約最適化問題 (COP)，最大制約充足問題 (Max-CSP) にも対応．
Java, Perl, MiniSat 等を別途インストールしておく必要あり．
他の SAT 型制約ソルバー: Azucar Web , BEE Web
3 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
概要 履歴 事例
Sugar の履歴
• 2002–2003 年 IPA 未踏プロジェクト (紀信邦 PM)
ジョブショップ・スケジューリング問題を SAT 符号化
して解くプログラムを開発． Sugar の原点
• 2006 年 順序符号化法を発表
• ILOG の 2005 年の論文で未解決だったオープンショッ
プ・スケジューリング問題の未解決問題 3 問の最適値を
決定することに成功．
• 2008 年 第 3 回制約ソルバー国際競技会
Web
に参戦し，全 10 部門中 4 部門で優勝．
• 2009 年 第 4 回制約ソルバー国際競技会
Web
に参戦し，全 7 部門中 3 部門で優勝．
4 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
概要 履歴 事例
Sugar を用いた事例紹介
• パッキング配列構成問題
[則武ほか,2012]
• 組合せテストのテストケース生成問題
[番原ほか,2010
DOI
; 番原ほか,2012]
• 釣合い型不完備ブロック計画構成問題
[松中ほか,2012
• ジョブショップ・スケジューリング問題
• 二次元矩形パッキング問題
• グラフ彩色問題
•
[田村ほか,2009
[宋ほか,2010
DOI
DOI
]
[越村ほか,2010]
DOI
]
]
他の事例：ラテン方格，時間割問題，多角形詰込み問題，パズル等
5 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
概要 履歴 事例
アウトライン
Sugar を用いた問題解法についてご紹介します．
符号化
CSP
SAT
SAT ソルバー
CSP の解
1
3
4
復号化
SAT の解
組合せテストのテストケース生成
SAT 符号化 (簡単に)
SAT ソルバー (簡単に)
6 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
概要 履歴 事例
アウトライン
Sugar を用いた問題解法についてご紹介します．
問題
モデリング
符号化
CSP
SAT
SAT ソルバー
CSP の解
復号化
1
組合せテストのテストケース生成
2
制約モデリング
3
4
SAT の解
(詳細に)
SAT 符号化 (簡単に)
SAT ソルバー (簡単に)
6 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
イベント順序テスト
Event-Sequence Testing
7 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
例えば
10 個のイベントを処理するシステムをテストしたい
• 網羅的テストは 10! = 3, 628, 800 (非現実的)
その代わりに，任意の 3 個のイベントに対して，すべての
可能な順序をカバーするテストを行う．
• 単純には 10 P3 = 8 × 9 × 10 = 720 テスト (順序) が必要．
• 1 回のテストで，最低 3 つの順序をカバーできるので，
テスト総数は 240 以下．
a b c d e f g h i j
• 実際には 1 回のテストで，もっとたくさんの順序をカ
バーできる．
720 通りの順序をカバーするテスト総数の最小値は？
8 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
答えは
• 11 テストでよい．
• この例は順序被覆配列 (SCA; Sequence Covering Array)
問題 [Kuhn,2010] に帰着．
SCA(11; 10, 3)
a
f
h
i
g
d
g
h
i
e
e
b
a
d
c
d
j
c
j
h
f
d
c
i
i
j
f
h
b
e
f
j
c
d
g
b
d
e
c
j
b
c
d
j
e
j
e
b
b
g
i
f
b
g
i
f
h
a
a
a
e
e
i
g
i
f
g
e
j
h
h
a
h
g
d
b
h
h
c
g
f
j
i
a
a
a
c
g
i
d
f
e
c
f
f
d
e
a
a
j
b
c
g
i
b
d
c
j
h
b
• テスト数 11, イベント数 10,
強さ 3
• 各行は 1 つのテストケース
• 各行は 10 個のイベントの順列
(順列制約)
• 任意の 3 個のイベントのすべ
ての可能な順序が少なくとも
1 回現れる (カバレッジ制約)
9 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
答えは
• 11 テストでよい．
• この例は順序被覆配列 (SCA; Sequence Covering Array)
問題 [Kuhn,2010] に帰着．
SCA(11; 10, 3)
a
f
h
i
g
d
g
h
i
e
e
b
a
d
c
d
j
c
j
h
f
d
c
i
i
j
f
h
b
e
f
j
c
d
g
b
d
e
c
j
b
c
d
j
e
j
e
b
b
g
i
f
b
g
i
f
h
a
a
a
e
e
i
g
i
f
g
e
j
h
h
a
h
g
d
b
h
h
c
g
f
j
i
a
a
a
c
g
i
d
f
e
c
f
f
d
e
a
a
j
b
c
g
i
b
d
c
j
h
b
• テスト数 11, イベント数 10,
強さ 3
• 各行は 1 つのテストケース
• 各行は 10 個のイベントの順列
(順列制約)
• 任意の 3 個のイベントのすべ
ての可能な順序が少なくとも
1 回現れる (カバレッジ制約)
9 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
値変数 位置変数 結合行列 実験
制約モデリング
問題
モデリング
符号化
CSP
SAT
SAT ソルバー
CSP の解
復号化
SAT の解
10 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
値変数を使うモデル
値変数 位置変数 結合行列 実験
[番原ほか,2012]
イベントの値 を表す変数 mr ,i ∈ {1, 2, 3, 4}
(1 ≤ r ≤ 6, 1 ≤ i ≤ 4)
SCA(6; 4, 3)
1
a
d
c
a
b
b
2
d
c
d
c
d
c
3
b
b
a
b
a
a
4
c
a
b
d
c
d
11 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
値変数を使うモデル
値変数 位置変数 結合行列 実験
[番原ほか,2012]
イベントの値 を表す変数 mr ,i ∈ {1, 2, 3, 4}
CSP
SCA(6; 4, 3)
1
a
d
c
a
b
b
2
d
c
d
c
d
c
(1 ≤ r ≤ 6, 1 ≤ i ≤ 4)
3
b
b
a
b
a
a
4
c
a
b
d
c
d
alldifferent (mr ,1 , mr ,2 , mr ,3 , mr ,4 )
ar ,(i,j,k),(p,q,u) = 1 ⇔ (mr ,i = p) ∧
(mr ,j = q) ∧
(mr ,k = u)
∑
ar ,(i,j,k),(p,q,u) ≥ 1
1≤r ≤6
1≤i<j<k≤4
where ar ,(i,j,k),(p,q,u) ∈ {0, 1}, 1 ≤ r ≤ 6, 1 ≤ i < j < k ≤ 4,
1 ≤ p, q, u ≤ 4, p ̸= q, p ̸= u, and q ̸= u.
• 順列制約はグローバル制約 alldifferent で表現．
∑
• カバレッジ制約は基数制約 i ℓi ▷ k で表現．
(ℓi ∈ {0, 1}, k は整数定数, ▷ ∈ {=, >, ≥, <, ≤})
11 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
位置変数を使うモデル
値変数 位置変数 結合行列 実験
[番原ほか,2012]
イベントの位置 を表す変数 xr ,i ∈ {1, 2, 3, 4}
(1 ≤ r ≤ 6, 1 ≤ i ≤ 4)
SCA(6; 4, 3) の位置表現
a b
1 3
4 3
3 4
1 3
3 1
3 1
c
4
2
1
2
4
2
d
2
1
2
4
2
4
12 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
値変数 位置変数 結合行列 実験
位置変数を使うモデル
[番原ほか,2012]
イベントの位置 を表す変数 xr ,i ∈ {1, 2, 3, 4}
SCA(6; 4, 3) の位置表現
a b
1 3
4 3
3 4
1 3
3 1
3 1
c
4
2
1
2
4
2
d
2
1
2
4
2
4
(1 ≤ r ≤ 6, 1 ≤ i ≤ 4)
CSP
alldifferent (xr ,1 , xr ,2 , xr ,3 , xr ,4 )
yr ,(i,j,k) = 1 ⇔ (xr ,i < xr ,j ) ∧
(xr ,i < xr ,k ) ∧
(xr ,j < xr ,k )
∑
yr ,(i,j,k) ≥ 1
r
where yr ,(i,j,k) ∈ {0, 1}, 1 ≤ r ≤ 6, 1 ≤ i, j, k ≤ 4, i ̸= j, i ̸= k,
and j ̸= k.
• 前モデルと同様に，alldifferent 制約と基数制約を使用．
• SCA のカバレッジ制約を簡潔に表現可能．
12 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
結合行列を使うモデル
値変数 位置変数 結合行列 実験
[番原ほか,2012]
結合行列 と呼ばれる (0, 1)-行列を使う．
• 各行は個々のテストケースでラベル付．
• 各列は任意の 3 個のイベントのすべての可能な順序でラベル付．
• 列 j が行 i の部分列のとき (i, j)-成分は 1, そうでなければ 0.
SCA(6; 4, 3) の結合行列
a a b b c c a a b b d d a a c c d d b b c c d d
b c a c a b b d a d a b c d a d a c c d b d b c
c b c a b a d b d a b a d c d a c a d c d b c b
a
d
c
a
b
b
d
c
d
c
d
c
b
b
a
b
a
a
c
a
b
d
c
d
13 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
結合行列を使うモデル
値変数 位置変数 結合行列 実験
[番原ほか,2012]
結合行列 と呼ばれる (0, 1)-行列を使う．
• 各行は個々のテストケースでラベル付．
• 各列は任意の 3 個のイベントのすべての可能な順序でラベル付．
• 列 j が行 i の部分列のとき (i, j)-成分は 1, そうでなければ 0.
SCA(6; 4, 3) の結合行列
a
d
c
a
b
b
d
c
d
c
d
c
b
b
a
b
a
a
c
a
b
d
c
d
a
b
c
1
0
0
0
0
0
a
c
b
0
0
0
1
0
0
b
a
c
0
0
0
0
1
0
b
c
a
0
0
0
0
0
1
c
a
b
0
0
1
0
0
0
c
b
a
0
1
0
0
0
0
a
b
d
0
0
0
1
0
0
a
d
b
1
0
0
0
0
0
b
a
d
0
0
0
0
0
1
b
d
a
0
0
0
0
1
0
d
a
b
0
0
1
0
0
0
d
b
a
0
1
0
0
0
0
a
c
d
0
0
0
1
0
0
a
d
c
1
0
0
0
0
0
c
a
d
0
0
0
0
0
1
c
d
a
0
0
1
0
0
0
d
a
c
0
0
0
0
1
0
d
c
a
0
1
0
0
0
0
b
c
d
0
0
0
0
0
1
b
d
c
0
0
0
0
1
0
c
b
d
0
0
0
1
0
0
c
d
b
0
0
1
0
0
0
d
b
c
1
0
0
0
0
0
d
c
b
0
1
0
0
0
0
• SCA のカバレッジ制約は，結合行列の各列の和が 1 以
上という制約に置換えられる (基数制約)．
13 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
値変数 位置変数 結合行列 実験
制約モデルの比較：CPU 時間 (秒)
SCA(n; s, t) SAT/UNSAT 結合行列 結合行列 位置変数
位置変数
位置変数
n
s
t
の別
(lex-row)
(snake lex) (double lex)
6
5
3
UNSAT
1.320 < 0.000
5.457
0.008
0.011
7∗ 5
3
SAT < 0.000 < 0.000
0.005
0.010
0.010
7
6
3
UNSAT 1327.350
0.110
T.O
0.383
0.588
∗
8
6
3
SAT
0.005
0.006
0.012
0.016
0.022
7
7
3
UNSAT 1442.410
0.180
T.O
1.921
5.509
∗
8
7
3
SAT
0.008
0.015
0.032
0.077
0.027
7
8
3
UNSAT
T.O
0.390
T.O
8.280
28.870
8∗ 8
3
SAT
0.070
0.094
7.870
2.815
18.160
9
9
3
SAT
0.075
0.242
6.139
6.070
64.570
9 10
3
SAT
11.896
5.890 982.580
1188.240
T.O
10 11
3
SAT
0.047
0.052
59.670
30.216
67.031
10 12
3
SAT
0.046
0.456 774.338
117.258
T.O
10 13
3
SAT
0.980
0.371
T.O
T.O
T.O
10 14
3
SAT
5.546
25.880
T.O
T.O
T.O
10 15
3
SAT 541.480 443.012
T.O
T.O
T.O
11 16
3
SAT
89.580 107.334
T.O
T.O
T.O
11 17
3
SAT
62.560
T.O
T.O
T.O
T.O
12 18
3
SAT
3.603
3.830
T.O
T.O
T.O
SAT
2.851
18.840
T.O
T.O
T.O
12 19
3
12 20
3
SAT
22.500 180.256
T.O
T.O
T.O
15 30
3
SAT 673.210 190.200
T.O
T.O
T.O
17 40
3
SAT 771.990
T.O
M.O
M.O
M.O
14 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
値変数 位置変数 結合行列 実験
制約モデルの比較：CPU 時間 (秒)
SCA(n; s, t) SAT/UNSAT 結合行列 結合行列 位置変数
位置変数
位置変数
n
s
t
の別
(lex-row)
(snake lex) (double lex)
6
5
3
UNSAT
1.320 < 0.000
5.457
0.008
0.011
7∗ 5
3
SAT < 0.000 < 0.000
0.005
0.010
0.010
7
6
3
UNSAT 1327.350
0.110
T.O
0.383
0.588
∗
8
6
3
SAT
0.005
0.006
0.012
0.016
0.022
7
7
3
UNSAT 1442.410
0.180
T.O
1.921
5.509
∗
8
7
3
SAT
0.008
0.015
0.032
0.077
0.027
7
8
3
UNSAT
T.O
0.390
T.O
8.280
28.870
8∗ 8
3
SAT
0.070
0.094
7.870
2.815
18.160
9
9
3
SAT
0.075
0.242
6.139
6.070
64.570
9 10
3
SAT
11.896
5.890 982.580
1188.240
T.O
10 11
3
SAT
0.047
0.052
59.670
30.216
67.031
10 12
3結合行列モデルが効率的かつスケーラブル
SAT
0.046
0.456 774.338
117.258
T.O
10 13
3
SAT
0.980
0.371
T.O
T.O
T.O
10 14
3
SAT
5.546
25.880
T.O
T.O
T.O
10 15
3
SAT 541.480 443.012
T.O
T.O
T.O
11 16
3
SAT
89.580 107.334
T.O
T.O
T.O
11 17
3
SAT
62.560
T.O
T.O
T.O
T.O
12 18
3
SAT
3.603
3.830
T.O
T.O
T.O
SAT
2.851
18.840
T.O
T.O
T.O
12 19
3
12 20
3
SAT
22.500 180.256
T.O
T.O
T.O
15 30
3
SAT 673.210 190.200
T.O
T.O
T.O
17 40
3
SAT 771.990
T.O
M.O
M.O
M.O
14 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
値変数 位置変数 結合行列 実験
既存研究との比較：SCAN(s, t) の上限値
結合行列
ASP
貪欲法
(Erdem ’11) (Kuhn ’10)
ASP Sugar 厳密 貪欲
5 3 7
7
7
−
8
6 3 8
8
8
−
10
7 3 8
8
8
−
12
8 3 8
8
8
−
12
9 3 9
9
9
−
14
9
9
11
14
10 3 9
11 3 10
10
10
−
14
12 3 10
10
10
−
16
13 3 10
10
10
−
16
14 3 10
10
10
−
16
15 3 10
10
10
−
18
16 3 11
11
11
−
18
17 3 11
11
11
−
20
18 3 12
12
−
−
20
12
−
−
22
19 3 12
20 3 12
12
−
19
22
s t
結合行列
ASP
貪欲法
(Erdem ’11) (Kuhn ’10)
ASP Sugar 厳密 貪欲
21 3 12
12
−
−
22
22 3 13
13
−
−
22
23 3 14
13
−
−
24
24 3 14
14
−
−
24
25 3 14
14
−
−
24
14
−
−
24
26 3 14
27 3 14
14
−
−
26
28 3 14
14
−
−
26
29 3 15
15
−
−
26
30 3 15
15
−
23
26
40 3 17
17
−
27
32
50 3 19
−
−
31
34
60 3 21
−
−
34
38
70 3 22
−
−
36
40
−
−
38
42
80 3 24
s t
15 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
値変数 位置変数 結合行列 実験
既存研究との比較：SCAN(s, t) の上限値
結合行列
s t
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
3
3
3
3
3
3
3
3
3
3
3
3
3
3
3
3
ASP
7
8
8
8
9
9
10
10
10
10
10
11
11
12
12
12
ASP
貪欲法
結合行列
ASP
貪欲法
(Erdem ’11) (Kuhn ’10)
s t
(Erdem ’11) (Kuhn ’10)
Sugar 厳密 貪欲
ASP Sugar 厳密 貪欲
7
7
−
8
21 3 12
12
−
−
22
8
8
−
10
22 3 13
13
−
−
22
8
8
−
12
23 3 14
13
−
−
24
8
8
−
12
24 3 14
14
−
−
24
9
9
−
14
25 3 14
14
−
−
24
9
9
11
14
26 3 14
14
−
−
24
結合行列モデルは既知の上限値を大きく更新
10
10
−
14
14
−
−
26
27 3 14
28 3 14
10
10
−
16
14
−
−
26
10
10
−
16
29 3 15
15
−
−
26
30 3 15
10
10
−
16
15
−
23
26
10
10
−
18
40 3 17
17
−
27
32
11
11
−
18
50 3 19
−
−
31
34
11
11
−
20
60 3 21
−
−
34
38
12
−
−
20
70 3 22
−
−
36
40
12
−
−
22
80 3 24
−
−
38
42
12
−
19
22
15 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
SAT
(Boolean Satisfiability Testing)
16 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
SAT
与えられた命題論理式 (節形式) について，充足する値割当
てが存在するか否かを判定する問題
• 理論上も実際上も計算機科学／人工知能の中心的課題
• NP 完全であることが初めて示された問題 [Cook,1971]
• 近年になって，SAT 問題を解く高速な SAT ソルバーが
開発された (MiniSat 等).
SAT ソルバーをバックエンドとして用いる SAT 型アプロー
チが困難な組合せ問題を解くための手法として広く用いら
れるようになっている．
17 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
SAT 型アプローチの例
• 有界モデル検査
[Biere,1999]
• プランニング (SATPLAN, Blackbox)
• 自動テストパターン生成
• ソフトウェア仕様 (Alloy)
[Kautz & Selman,1992]
[Larrabee,1992]
[1998]
• ソフトウェアパッケージの依存性解析 (SATURN)
• 書換え系 (Aprove, Jambox)
• 解集合プログラミング (clasp, Cmodels-2)
• 一階論理の定理証明系 (iProver, Darwin)
• 一階論理のモデル発見機 (Paradox)
• 制約充足問題 (Sugar, Azucar, BEE)
18 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
分類 基準 alldifferent
SAT 符号化
問題
モデリング
符号化
CSP
SAT
SAT ソルバー
CSP の解
復号化
SAT の解
19 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
分類 基準 alldifferent
SAT 符号化法の分類
整数変数の符号化法に着目すると，4 つに分類される．
• 順序系
各整数変数 x と各整数定数 a ∈ Dom(x) に対して，
x ≤ a を意味する命題変数 p(x ≤ a) を用いる方法
• 直接系
各整数変数 x と各整数定数 a ∈ Dom(x) に対して，
x = a を意味する命題変数 p(x = a) を用いる方法
• 対数系
各整数変数 x の 2 進表現に着目し，x の i 桁目が 1 に等
しいことを意味する命題変数 p(x (i) ) を用いる方法
• 混合系
順序系と直接系の両方の命題変数を用いる．
20 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
分類 基準 alldifferent
主な SAT 符号化法
順序系
直接系
順序符号化法 [田村ほか,2006
コンパクト順序符号化法 ∗
直接符号化法
支持符号化法
多値符号化法
DOI
]
[丹生ほか,2011
[de Kleer,1989; Walsh,2000
[Kasif,1990
DOI
DOI
DOI
]
; Gent,2002]
[Selman,1992]
対数系
対数符号化法 [岩間・宮崎,1994 ; Van Gelder,2008
対数支持符号化法 [Gavanelli,2007 DOI ]
混合系
正規符号化法 [Béjar,Hähnle & Manyà,2001]
ラダー符号化法 [Gent,2004]
∗
]
DOI
]
対数系とも言える
21 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
分類 基準 alldifferent
SAT 符号化法の良し悪し
問題の性質，利用する SAT ソルバーの特性によって異なる
ため明確な基準はないが，以下の基準がよく用いられる † ．
SAT 符号化法の評価基準
• 符号後の節数．一般に少ない方が良いとされる．そもそも大
きすぎるとメモリにのらない．
• 符号化後の SAT 問題に対する SAT ソルバーの単位伝播と元
の CSP に対する制約伝播との関連
個人的な意見
• 整数変数のドメインが 103 以下ならば，順序符号化法 (Sugar, BEE)
• それ以上なら，コンパクト順序符号化法 (Azucar) か対数符号化法
• 確率的ソルバーを使うのであれば，多値符号化法
†
田村直之, 丹生智也, 番原睦則. 制約最適化問題と SAT 符号化. 人工知能学会誌, 25(1):77-85, 2010
CiNii
22 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
分類 基準 alldifferent
グローバル制約の符号化 (Sugar の場合)
• alldifferent (x1 , x2 , . . . , xn ) は，以下の制約式に置換さ
れた後，SAT に符号化される． (lb と ub は整数変数の上下限)
∧
(x ̸= xj )
∧ i<j i
¬ ∧ (xi < lb + n − 1)
¬ (xi > ub − n + 1)
最後の 2 つの制約式は，互いに異なる n 変数が n − 1 の
サイズのドメインに入らないことを表す [田島・田
村,2007]．(鳩の巣原理の応用)
• 基数制約 の SAT 符号化は重要な研究課題であり，
MaxSAT 等への応用がある．
[Bailleux & Boufkhad,2003
Codish & Zazon-Ivry,2010
DOI
DOI
; Sinz,2005
DOI
; Ası́n ほか,2011
;
DOI
]
23 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
概要 競技会 比較実験
SAT ソルバー
問題
モデリング
符号化
CSP
SAT
SAT ソルバー
CSP の解
復号化
SAT の解
24 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
概要 競技会 比較実験
SAT ソルバー
与えられた命題論理式 (節形式) が充足可能 (SAT) か充足不
能 (UNSAT) かを判定するプログラム．
• 答えが SAT の場合，値割当てを解として出力する．
系統的ソルバー
SAT と UNSAT のいずれも判定可能．
多くは DPLL アルゴリズムに基づく．
[Davis & Putnam,1960 ; Davis, Logemann & Loveland,1962]
確率的ソルバー
SAT のみ判定可能．
UNSAT は一般に判定できない．
確率的局所探索を用いる．
ポートフォリオ型 複数のソルバーを組み合わせて
SAT 問題を解く．
25 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
概要 競技会 比較実験
最新の CDCL SAT ソルバー
最新技術が DPLL に導入され，大幅な性能向上が実現
•
•
•
•
•
矛盾からの節学習 (CDCL; Conflict Driven Clause Learning)[Silva,1996]
非時間順バックトラック法 [Silva,1996]
ランダム・リスタート [Gomes,1998]
監視リテラル [Moskewicz & Zhang,2001]
変数選択ヒューリスティック [Moskewicz & Zhang,2001]
• Chaff と zChaff は 1 桁から 2 桁の速度改善を実現 [2001]
• SAT 競技会および SAT レースが 2002 年から毎年開催され，
SAT ソルバーの実装技術の進歩に大きく貢献．
• MiniSat Web [Eén & Sörensson,2003] は C++で 1000 行
以内
• 最近の SAT 競技会では，MiniSat 系と呼ばれる MiniSat ベー
スのソルバーが上位を占める．
26 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
概要 競技会 比較実験
SAT 競技会 2011 の優勝ソルバー (CPU 時間)
Application 部門
SAT+UNSAT
Glucose
SAT
contrasat
UNSAT
GlueMiniSat
Crafted 部門
3S
Web
3S
ppfolio
Web
Random 部門
Web
clasp
sparrow2011
march rw
• MiniSat 系は Application 部門を独占
しており，実際の応用問題に強いソ
ルバーである．
• ポートフォリオ型 は 3 部門で優勝し
ており，平均的な強みがある万能型
のソルバーである．
• 実時間での評価では，優勝ソルバー
の殆どをポートフォリオ型が占める．
GlueMiniSat [鍋島,2010] が獲得したメダル
個人的な意見
• MiniSat −→ Glucose −→ clasp の順で試す．
• UNSAT 問題ならば，GlueMiniSat
27 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
概要 競技会 比較実験
SAT ソルバーの比較
Handbook of Satisfiability (IOS Press, 2009) 第 17 章にある未解決問題 (6 問)
•
•
•
t
t
k g Question Open/Closed
2
8 3
b = 12?
Closed
2
2
7 4
5 6
b ≤ 20?
b ≤ 38?
Open
Open
3 12 2
b = 14?
Closed
3
3
b ≤ 32?
b ≤ 87?
Closed
Open
5 3
7 4
備考
[Colbourn ほか,2010
[番原ほか,2010]
DOI
]
[Colbourn ほか,2010 DOI ]
[番原ほか,2010 DOI ]
[Bulutoglu and Margot,2008
DOI
組合せテストのテストケース生成問題 (CA(b; t, k, g ) 問題)
DOI ]
制約モデル：Hnich らのモデル [Hnich ほか,2006
SAT 符号化：順序符号化法 (O.E.)，混合符号化法 (M.E.) [番原ほか,2010
k g
2 8 3
2 7 4
3 12 2
3 13 2
b Result
12
20
14
15
UNSAT
UNSAT
UNSAT
UNSAT
]
DOI
]
GlueMiniSat 2.2.5
Glucose 2.0
MiniSat 2.2.0
O.E.
M.E.
O.E.
M.E.
O.E.
M.E.
T.O 1,233,375
T.O
T.O
T.O
T.O
1,446,275
T.O
T.O
T.O
T.O
T.O
2,977
2,256
2,128
2,585 17,958 18,713
472,098
210,252 589,901 1,674,122
T.O
T.O
(単位：秒，タイムアウト：20 CPU 日)
28 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
まとめ
Sugar を用いた問題解法についてご紹介しました．
1
制約モデリング
• 値変数，位置変数，結合行列，(複合変数)
• alldifferent 等のグローバル制約
2
3
SAT 符号化
SAT ソルバー
29 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
ご清聴ありがとうございました．
30 / 31
Knuth 先生 Sugar SCA モデル SAT 符号化 ソルバ まとめ
Sugar のダウンロード
ぜひ使ってみてください
http://bach.istc.kobe-u.ac.jp/sugar/
Web
パズル好きの方へ
• パズルを Sugar 制約ソルバーで解く
• http://bach.istc.kobe-u.ac.jp/sugar/puzzles/ Web
• 数独，カックロ，美術館，四角に切れ，ナンバーリン
ク，ましゅ，スリザーリンク，橋をかけろ，ヤジリン，
ぬりかべ，ひとりにしてくれ，フィルオミノ，へやわ
け，お絵かきロジック
• プログラム不要の「制約プログラミング手習い」
• http://karetta.jp/book/withoutprogramming Web
• 藤原さんが Sugar を使って，色々なパズルを解いている
Web ページ．
31 / 31