2013 Fiscal Year Annual Research Report
形式論理のプロパティー検査と発見による計算限界の解析
Publicly Offered Research
| Project Area | A multifaceted approach toward understanding the limitations of computation |
|---|
| Project/Area Number |
25106501
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Innovative Areas (Research in a proposed research area)
|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2013-04-01 – 2015-03-31
|
| Keywords | 記述計算量 / 計算量理論 / 形式論理 / 有限モデル理論 / プログラム合成 |
|---|
| Research Abstract |
計算機科学では、形式論理が中心的な役割になっている。論理の記述能力を研究する記述計算量が本領域の中心になる計算量理論と同型である。そこでは帰着やプログラム等を論理式として表し、計算問題の複雑さをその問題を定義する時必要な記述能力で定義する。
本研究では、ある様子を説明する論理式の発見等を課題にする。人工知能等の応用も数多くあるが、ここでは論理式の発見に関する基本的なアルゴリズムや理論をはじめ、論理式として表せる計算量理論の帰着等での応用を目的とする。このような論理式を効率的に発見ができるなら、計算量理論の面白い成果が得られる。または、効率的に評価できない論理式と効率の良い同等な論理式を発見できる応用も考えられる。これはプログラム合成の論理バージョンになる。
今年度の主な研究実績は次のようになっている。まずは、ある様子を説明する論理式を発見するための理論的な機械学習モデルを提案し、いくつかの応用を挙げている。しかし、理論的なモデルだけではなく最新のSATやQBFソルバを利用し基本的なアルゴリズムを実装し、いくつか応用もしている。例えば、計算量理論の帰着を発見するためのツール、プログラム合成や新しいボードゲームを自動的に学習するツールを開発し公開している。以上述べたようにSAT、QBFやASPソルバを利用することが多いので、このような応用においてたくさんのソルバを比較している。
以上の成果をまとめ、国際会議等で発表している。その結果はSAT/QBF等のコミュニティと共同研究が始まり、これからの研究実績も期待できる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の目的は前述した論理式の発見に関する応用や基本的なアルゴリズム、及び論理式の効率的な計算（プロパティー検査等）になる。両方のテーマが本領域と関係が強い。
第一年度において、論理式の発見に関するテーマが予想以上研究が進み、共同研究者の都合もあったためこのテームに集中した。従って、論理式の発見に関する論理的な機械学習モデル、基本的なアルゴリズムとその実装、様々な応用等が計画以上進展している。計算量理論の帰着をはじめ、プログラム合成等の応用も計画以上進んでいる。ボードゲーム等の応用もしたが、本領域の中心になる計算量理論の応用が予想以上進んでいる。
第一年度の研究成果を国際会議等で発表し、国際的に交流をし共同研究をしている。有限モデル理論・計算量理論のコミュニティとの関係の引き続きやSAT・QBFのコミュニティとの新しい関係ができ共同研究も始まった。その関係の始まりになったのが第一年度の研究業績であり、当初研究目的以上進んでいる。
このような課題だと様々な論理式や離散構造を効率的に取り扱う必要がある。第一年度は論理式の発見に集中したため、プロパティー検査のような理論的な成果より論理式の発見に関する実際の実装や応用で必要なものに集中した。
以上のように論理式の発見に関しては予定以上進んでいる。このテーマに関しては理論的なモデル、基本的なアルゴリズムとその実装、当初研究計画の応用等は予定以上進んでいる。このテーマに集中したため、論理式の効率的な扱いに関してプロパティー検査のような理論的な成果より論理式の発見で必要なものに集中した。
|
| Strategy for Future Research Activity |
本研究の目的は前述した論理式の発見に関する応用や基本的なアルゴリズム、及び論理式の効率的な計算（プロパティー検査等）になる。以上述べたように本年度は計算量理論の帰着や、プログラム合成、ゲーム等の応用を含み、論理式の発見に関する基本的なアルゴリズムと実装の研究が予定以上の進達はあった。その成果のかげで、SAT・QBFのコミュニティと新しい関係もでき、今後はそのコミュニティとも共同研究を進む。
計算量理論の理論的な成果になるような論理式を発見することを目指す。そのような問題に関しては基本的なアルゴリズムと実装はできているが、重要な問題に対して効率性が足りない。従って、並列と分散アルゴリズムやSAT・QBFソルバが課題になる。例えば、分散QBFソルバは現在手に入らないため、QBFのコミュニティと共同研究課題にもなる。
また、本領域の陰でスーパーコンピュータが利用できるようにもなったので、大規模なシステムで分散ソルバ等を用いて論理式の発見をすることについても考える。効率的な分散ソルバがあまりないため、ソルバを開発することも考えられる。分散SATとQBFソルバの開発や論理式の発見において分散アルゴリズムを用いて理論的に重要な問題を目指すこと等、今年度の研究業績は今後の研究の根になる。
もちろん、SAT・QBFコミュニティだけではなく有限モデル理論や計算量理論のコミュニティとの関係の引き続きや本領域の計画研究班等と連携し研究を進む。
|
-
-
-
-
-
-
-
-
[Presentation] Benchmarks from Reduction Finding2013
Author(s)
Charles Jordan and Lukasz Kaiser
Organizer
International Workshop on Quantified Boolean Formulas 2013 (QBF 2013), Informal Workshop Report, pp. 40-43
Place of Presentation
University of Helsinki (Finland)
Year and Date
20130609-20130609
-
