スライド 1

k-SATアルゴリズムの
実験的性能評価
西関研究室 8668
高木康彰
研究背景
• 充足可能性問題(SAT)は計算機科学における最も基本的な
問題
• 論理合成,システム検証,スケジューリング問題など様々な分
野に応用されている
• SATを高速に解くアルゴリズムの研究がされている
• k-SATを解くアルゴリズムに本研究で提案したヒューリスティッ
クスを用いると,どれだけ高速化できるのか？
充足可能性問題(SAT)
• CNF論理式が与えられたとき、その論理式を充足させる変数
の割り当てが存在するかどうかの判定問題
全ての変数にtrueを割り当てるとF1はtrue
Yesを出力
変数にどんな割当を行ってもF2はfalse
Noを出力
充足可能性問題(SAT)
• 与えられる論理式の各節に含まれる変数の個数が高々k個のSAT
k-SAT
例：
3-SAT
x  x  x  x  x  x  x  x  x  ...
1
2
3
1
2
4
4
5
6
4-SAT
x  x  x  x  x  x  x  x  x  x  x  x  ...
1
• SAT,
2
3
4
1
であるk-SATはNP完全
2
5
6
3
5
7
8
Schöningのアルゴリズム
• 入力 : F (n個の変数を持つk-CNF論理式)
• 出力 : Yes/No
(1)以下を指定された回数繰り返す
(1.1)n個の変数の初期割り当てa∈{0,1}ｎをランダムに選ぶ
(1.2)以下を3n回繰り返す
(1.2.1)aで Fが充足しているなら, Yesを出力し終了
(1.2.2)aで充足していない節Cを任意に選ぶ
(1.2.3)節Cの中の変数xをランダムに選び、フリップして
割当aを更新
(2)Noを出力
Heuristic1
• 入力 : F (n個の変数を持つk-CNF論理式)
• 出力 : Yes/No
(1)以下を指定された回数繰り返す
(1.1)n個の変数の初期割り当てa∈{0,1}ｎをランダムに選ぶ
(1.2)以下を3n回繰り返す
(1.2.1)aで Fが充足しているなら, Yesを出力し終了
(1.2.2)aで充足していない節Cを任意に選ぶ
(1.2.3)節Cの変数でフリップ後に充足する節数が一番多
い変数一つをフリップして,割当aを更新
(2)Noを出力
Heuristic2
• 入力 : F (n個の変数を持つk-CNF論理式)
• 出力 : Yes/No
(1)以下を指定された回数繰り返す
(1.1)n個の変数の初期割り当てa∈{0,1}ｎをランダムに選ぶ
(1.2)以下を3n回繰り返す
(1.2.1)aで Fが充足しているなら, Yesを出力し終了
(1.2.2)aで充足していない節Cを任意に選ぶ
(1.2.3) 節Cのk個の変数の一部か全部をフリップして
充足する節数が一番多くなるように割当aを更新
(2)Noを出力
実験1 : 概要
• 変数の個数 : n=20, 節の個数 : c=91,
n=50,
c=218,
n=100,
c=430,
このような3-SAT入力例題を用意
1000例
1000例
100例
• 入力例題は全て充足解を持つ
• 3つのアルゴリズムを実行し,充足解を得るまでの
計算時間, 初期割当回数を計測し,比較する
• 使用機器 CPU : Core i7 i7-870 2.93GHz
メモリ : 4.00GB
OS : Windows7
実験1 : 結果
計算時間
秒
初期割当回数
回数
10000
10000000
1000
1000000
100
100000
10
Schöning
10000
Schöning
1
Heuristic1
1000
Heuristic1
Heuristic2
0.1
Heuristic2
100
10
0.01
1
0.001
20
50
変数の個数 : n
100
20
50
100
変数の個数 : n
• 入力例題の変数の個数が50, 100のとき、
ヒューリスティックスを用いた2つは高速に解を得ている
実験2 : 概要
• 変数の個数は50
• 節数を200から1500まで100ずつ増加させ
100例ずつ計算時間と初期割当回数を計測
• 例題は全て充足解を持つ3-SAT
• 使用機器 CPU : Core i7 i7-870 2.93GHz
メモリ : 4.00GB
OS : Windows7
実験2 : 結果
1500
1400
1300
1200
1100
1000
Heuristic2
900
1500
1400
1300
1200
1100
1000
900
800
700
600
500
400
300
200
0
Heuristic1
700
2
Schöning
600
4
500
6
400
8
300
10
1800
1600
1400
1200
1000
Schöning 800
600
Heuristic1
400
Heuristic2 200
0
200
12
節数 : c
割当回数
回数
800
計算時間
秒
節数 : c
Schöningのアルゴリズムは節数が増えると解を得るまで時間がかかる
ランダムに変数をフリップしても充足しない節数が増えることが多い
実験2 : 結果
秒
計算時間
0.45
0.4
0.35
0.3
0.25
0.2
0.15
0.1
0.05
0
割当回数
回数
30
25
20
15
Heuristic1
Heuristic2
Heuristic1
10
Heuristic2
5
節数
1500
1400
1300
1200
1100
1000
900
800
700
600
500
400
300
200
0
節数
•
ヒューリスティックスを用いたアルゴリズムは節数が増えるほど高速に解を得ている
– ヒューリスティックスの効果が大きくなり、充足解を得やすくなっている
•
ヒューリスティックスを用いた2つは,ほとんどの節が充足しているとき、同じ探索路を
繰り返し巡回する場合がある
– 一度に複数の変数をフリップするHeuristic2の方がこれに陥りやすい
まとめ
• Schöningのアルゴリズムと比較して,ヒューリスティックスを用
いたアルゴリズムは,変数,節数が多い3-SATを高速に解く
– 50変数の場合に約9倍、100変数の場合に約150倍の高速化を達成
• 貪欲なヒューリスティックスを用いる場合、フリップする変数
の個数は一つの方が望ましい
• 今後の課題としては同じ初期割当を与えた場合の比較実験
やアルゴリズムの理論的な解析があげられる
既存のヒューリスティックスとの違い
• SATを局所探索で解くアルゴリズムにはあまりヒュー
リスティックスは用いられていない
– ヒューリスティックスは主に探索域の削減を目的
• 既存のヒューリスティックス
– 充足していない節全体で最も多く含まれている変数をフ
リップ
乱数生成について
• Mersenne Twister
– 疑似乱数生成アルゴリズム
• 長周期, 高次元均等分布
• 生成速度が速い
実験データ
• 実験1
SATLIB - Benchmark Problemsから引用
• 実験2
入力式生成アルゴリズムで作成
入力式生成アルゴリズム
• パラメータ : 変数の個数 : n
節の個数 : c
各節に含まれる変数の個数 : k
(1)n個の変数の充足解a*∈{0,1}ｎをランダムに選ぶ
(2)以下をc個の節に対して行う
(2.1)k個の変数
をランダムに選ぶ
(2.2)k個の変数及びその否定形からなる2k通りの組
み合わせから, a*で充足する組み合わせ一つをラン
ダムに選び,その節はそれらの論理和とする
(3)C個の節の論理積を論理式として出力
SATソルバー
• SATソルバは2種類
– 確率的な探索をする事で、素早く充足可能性を見つける。
しかし充足不可能性は見出せない
– 虱潰しに探索域を削っていき、最終的に充足可能か
充足不可能か判断可能
• 現在はDPLLアルゴリズムをベースにしたものが主流
Heuristic
Heuristic1/Heuristic2で遷移可能
Heuristic2のみ遷移可能
ex)100個の節を持つ論理式が与えられた場合
a*(充足解)
100
a1
99
98
97
充足している節の個数
a3
a2
a4
a(現在の割当)

Download Report