公募研究
新学術領域研究(研究領域提案型)
本研究では、ある様子を説明する形式論理式の発見等を課題にする。人工知能等の応用も数多くあるが、ここでは論理式の発見に関する基本的なアルゴリズムや理論をはじめ、論理式として表せる計算量理論の帰着等での応用を目的とする。昨年度はこのような基本的なアルゴリズムや帰着等を含む様々な応用について研究した。今年度はさらに複雑な問題を目指し、大規模な計算機等に集中した。形式論理式の発見について予想以上研究が進み、当初想像していなかった成果や課題もできた。特に、本領域に参加できたおかげで、東工大の大規模な高速スーパーコンピューターTsubameにアクセス可能になった。論理式の発見について簡単な応用や問題もあるが、理論的に面白い課題を目指すと理論的にも経験的にも難しい計算問題になる。難しい計算問題とスパコンは自然な組み合わせだが、本研究において必要な分散ソルバは存在しなかったため、最初のオープンソース分散QBFソルバを共同で開発し、スーパーコンピューター上で大規模な問題について研究した。QBFソルバは本研究以外にも応用が数多くあるため、他の研究や応用で利用されると期待している。本年度の主な研究業績は次のようになっている。まずはQBFソルバの専門家と共同でオープンソース分散QBFソルバを開発し、国際会議(SAT)で発表し、公開している。以上述べたように、オープンソース分散QBFソルバとして最初になるため、他の分野において従来できなかった応用がクラスターや並列マシン等が利用できるため、並列ソルバがあるのは喜ばしいことである。また、SATやQBFのコミュニティと連携し、本研究の問題が国際競争で用いるベンチマーク問題として認められた。従って、今後のソルバはこのような問題に対して効率化されると期待している。本年度の研究の一部はまだ査読中のため、報告には間に合わないが、当初の予定以上進んだと思っている。
26年度が最終年度であるため、記入しない。
すべて 2014 2013 その他
すべて 雑誌論文 (2件) (うち査読あり 2件、 謝辞記載あり 1件) 学会発表 (11件) 備考 (3件)
Theory and Applications of Satisfiability Testing, SAT 2014, Proceedings, Lecture Notes in Computer Science
巻: 8561 ページ: 430-437
10.1007/978-3-319-09284-3_32
Theory and Applications of Satisfiability Testing, SAT 2013, Proceedings, Lecture Notes in Computer Science
巻: 7962 ページ: 192-207
10.1007/978-3-642-39071-5_15
http://www-alg.ist.hokudai.ac.jp/~skip/index.html
http://toss.sourceforge.net/reduct.html
http://www-alg.ist.hokudai.ac.jp/~skip/index-j.html
