| 研究課題/領域番号 |
17700135
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
知能情報学
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
長井 歩 群馬大学, 工学部, 助手 (70375567)
|
|---|
| 研究期間 (年度) |
2005 – 2006
|
| 研究課題ステータス |
完了 (2006年度)
|
| 配分額 *注記 |
2,400千円 (直接経費: 2,400千円)
2006年度: 700千円 (直接経費: 700千円)
2005年度: 1,700千円 (直接経費: 1,700千円)
|
|---|
| キーワード | SAT / DPLL / CNF / BCP / xChaff |
|---|
| 研究概要 |
今日ではSATソルバーは、回路の等価性検証、モデル検査など、幅広い分野で探索エンジンとして用いられている。それらの実用性の高い問題に対して用いられるSATソルバーの殆んどはDPLLアルゴリズムをベースにしている。DPLLアルゴリズムには、この10年ほどの間に多種多様なアイデアが付加されている。近年のDPLLベースの探索アルゴリズムでは、仮定に仮定を重ね、探索中に矛盾を導いては、それを回避するための制約条件を積極的に学習することによって探索範囲を狭める仕組みになっている。DPLLでは、ある種の制約条件を学習する際に、今までの探索をすべて放棄して、rootまで戻ることになっている。
本年度の研究では、まず実用的にはその状況の際に、いつもrootまで戻るのが良いとは限らないことを明らかにした。学習内容が重要であることは言うまでもないが、それに至る探索過程もそれなりに尊重しても良い、ということである。その上で、rootまで遡るのではなく、ある簡単なヒューリスティックスに従って途中まで探索を戻す手法を提案した。提案手法の有効性の実験的確認として、SATの世界最大規模のコンペティションである、SAT Race 2006の問題に対して適用し、若干ながら提案手法の優位性が認められた。提案手法は、ここで問題としている、ある種の制約条件の学習という状況が発生しなければ、従来法と全く同じ振る舞いになるので、従来法に比べて大きな欠点はない。
|
