2012 Fiscal Year Annual Research Report
大規模ＳＡＴ問題解決のためのＥＰＲプルーバーに関する研究
| Project/Area Number |
21300054
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
長谷川 隆三 九州大学, システム情報科学研究科(研究院, 教授 (20274483)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
藤田 博 九州大学, システム情報科学研究科(研究院, 准教授 (70284552)
越村 三幸 九州大学, システム情報科学研究科(研究院, 助教 (30274492)
力 規晃 徳山工業高等専門学校, その他部局等, 助手 (50290804)
|
|---|
| Project Period (FY) |
2009-04-01 – 2013-03-31
|
| Keywords | モデル生成法 / SAT / MaxSAT / 基数制約 / 並列化 / 戦略の統合 |
|---|
| Research Abstract |
本年度は，(A) モデル生成型SATソルバーにおける学習節の分岐利用判定手法と削除戦略，(B) SATソルバーの各種戦略の統合による高速化，(C) fork機能によるSATソルバーの並列化，(D) SATソルバーによるラムゼー数の求解，(E) 基数制約を用いたMaxSATソルバー，について研究を進め，4件の査読付論文の公表，4件の学会発表を行った．以下，(A)～(E)のあらましを述べる．(A) 分岐の元となる正リテラルの出現数に着目し，出現数が少ない正リテラルを含む学習節を優先的に分岐に用いると性能が向上することを定量的に確かめた．学習節の削除戦略については，積極的削除から消極的削除まで５通りの削除戦略を用いた実験を行い，消極的に削除すると学習節が溜まり過ぎ性能が劣化することが分かった．(B) 充足可能な問題に強いSPhaseと充足不能な問題に強いUPhaseを交互に実行するPhase Shiftingの様々な改良を行った．実験の結果，高速ソルバーGlucoseを超える性能を確認した．(C) UNIXのシステムコールforkを利用して，SATソルバーminisat2.2の並列化を行った．学習節の共有を行わないue版と共有を行うsc版を実装し比較実験を64コアマシンを用いて行った．平均的にはue版の性能が良かった．(D) 制約節を導入し実行が進むにつれて制約を緩和していく手法により，ラムゼー数R(4,8)の下界をこれまでの56から58に上げることに成功した．(E) MaxSATソルバー競技会Max-SAT 2012に参加し，Partial MaxSAT部門のIndustrialとcraftedの双方で優勝した．
|
| Current Status of Research Progress |
Reason
24年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
24年度が最終年度であるため、記入しない。
|
