2014 Fiscal Year Annual Research Report
形式論理のプロパティー検査と発見による計算限界の解析
Publicly Offered Research
| Project Area | A multifaceted approach toward understanding the limitations of computation |
|---|
| Project/Area Number |
25106501
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2013-04-01 – 2015-03-31
|
| Keywords | 記述計算量 / プログラム合成 / 分散QBFソルバ / 並列QBFソルバ / 計算量理論 / 形式論理 / 有限モデル理論 |
|---|
| Outline of Annual Research Achievements |
本研究では、ある様子を説明する形式論理式の発見等を課題にする。人工知能等の応用も数多くあるが、ここでは論理式の発見に関する基本的なアルゴリズムや理論をはじめ、論理式として表せる計算量理論の帰着等での応用を目的とする。昨年度はこのような基本的なアルゴリズムや帰着等を含む様々な応用について研究した。今年度はさらに複雑な問題を目指し、大規模な計算機等に集中した。
形式論理式の発見について予想以上研究が進み、当初想像していなかった成果や課題もできた。特に、本領域に参加できたおかげで、東工大の大規模な高速スーパーコンピューターTsubameにアクセス可能になった。論理式の発見について簡単な応用や問題もあるが、理論的に面白い課題を目指すと理論的にも経験的にも難しい計算問題になる。
難しい計算問題とスパコンは自然な組み合わせだが、本研究において必要な分散ソルバは存在しなかったため、最初のオープンソース分散QBFソルバを共同で開発し、スーパーコンピューター上で大規模な問題について研究した。QBFソルバは本研究以外にも応用が数多くあるため、他の研究や応用で利用されると期待している。
本年度の主な研究業績は次のようになっている。まずはQBFソルバの専門家と共同でオープンソース分散QBFソルバを開発し、国際会議(SAT)で発表し、公開している。以上述べたように、オープンソース分散QBFソルバとして最初になるため、他の分野において従来できなかった応用がクラスターや並列マシン等が利用できるため、並列ソルバがあるのは喜ばしいことである。また、SATやQBFのコミュニティと連携し、本研究の問題が国際競争で用いるベンチマーク問題として認められた。従って、今後のソルバはこのような問題に対して効率化されると期待している。本年度の研究の一部はまだ査読中のため、報告には間に合わないが、当初の予定以上進んだと思っている。
|
| Research Progress Status |
26年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
26年度が最終年度であるため、記入しない。
|
-
-
-
[Presentation] QBF Gallery2014
Author(s)
Charles Jordan, Martina Seidl
Organizer
Theory and Applications of Satisfiability Testing (SAT 2014)
Place of Presentation
Vienna University of Technology (Austria)
Year and Date
2014-07-17 – 2014-07-17
-
-
-
-
