論理式の探索と自動合成による計算限界解析

• Project Area: A multifaceted approach toward understanding the limitations of computation
• Project/Area Number: 15H00847
• Research Category: Grant-in-Aid for Scientific Research on Innovative Areas (Research in a proposed research area)
• Allocation Type: Single-year Grants
• Review Section: Science and Engineering
• Research Institution: Hokkaido University
• Principal Investigator: ジョーダン チャールズハロルド 北海道大学, 情報科学研究科, 助教 (60647577)
• Project Period (FY): 2015-04-01 – 2017-03-31
• Project Status: Completed (Fiscal Year 2016)
• Budget Amount: ¥4,940,000 (Direct Cost: ¥3,800,000、Indirect Cost: ¥1,140,000); Fiscal Year 2016: ¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000); Fiscal Year 2015: ¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
• Keywords: 記述計算量 / 並列計算 / 分散計算 / 機械学習 / 知識発見 / 機会学習

Outline of Annual Research Achievements

本研究では記述計算量に基づき様々な論理式の探索と自動合成について一般的なモデルとそれに関するアルゴリズム・応用を課題にした。近年記述計算量をプログラム合成や形式検証で応用する研究がいくつかあるが、本研究ではそれらをunifyする一般的なモデルを大きな目的の一つにしている。つまり、計算量の帰着やプログラム合成など応用毎に最初からやり直すのではなく、一般的なモデルと実装の応用として簡単に利用できることを目的にしている。
本研究で得た主な成果は3つに分ける。まずは、最初から目的にしていた上記の一般的なモデルの提案とそれに関する基本的な性質を証明した。このモデルでは、従来の関連研究で使われた論理だけではなく、実数を扱える論理に拡張することによって、ニューラルネットワークや重み付きのグラフも取り扱えるようになった。
次は、このモデルを実装する時必要になる道具の一つであるQBFソルバに関していくつか成果もできた。特に、本領域に参加することによって、大規模なスパコンTsubameを利用することができて、並列計算や新しいQBF技術に関する研究ができて、複雑な合成問題などに応用することができる。最後は新学術領域に参加することによって、本領域に参加している研究者と議論したり新しい共同研究もできた。
それで本領域に参加できたおかげで、当初想像していなかった成果ができ、今後の研究に強く影響を与える。特に、本領域で初めて会った共同研究者と本領域で利用できたスパコンの組み合わせで新しい共同研究が生まれ、スパコンなど大規模な計算機で使える高速なフリーソフトを公開し、他分野の研究者が現在利用している。従来のものより千倍以上速くなる場合もあり、今まで解けなかった計算問題が解けるようになったので、計算限界をプッシュしている課題の一つになる。査読は何年間かかるものもあるため、論文はarXivなどで公開している。

Research Progress Status

28年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

28年度が最終年度であるため、記入しない。

Research Products

• [Journal Article] The Kahr-Moore-Wang Class Contains Untestable Properties (2016)
  • Author(s): Charles Jordan and Thomas Zeugmann
  • Journal Title: Baltic Journal of Modern Computing Volume: 4 Issue: 4 Pages: 736-752
  • DOI: 10.22364/bjmc.2016.4.4.11
  • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] A parallel framework for reverse search using mts (2016)
  • Author(s): David Avis and Charles Jordan
  • Journal Title: arXiv:1610.07735 Volume: なし
  • Acknowledgement Compliant
• [Journal Article] Machine Learning with Guarantees using Descriptive Complexity and SMT Solvers (2016)
  • Author(s): Charles Jordan and Lukasz Kaiser
  • Journal Title: arXiv:1609.02664 Volume: なし
  • Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] QBF Gallery 2014: The QBF Competition at the FLoC 2014 Olympic Games (2016)
  • Author(s): Mikolas Janota, Charles Jordan, Will Klieber, Florian Lonsing, Martina Seidl and Allen Van Gelder
  • Journal Title: Journal on Satisfiability, Boolean Modeling and Computation Volume: 9 Pages: 187-206
  • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] mplrs: A scalable parallel vertex/facet enumeration code (2015)
  • Author(s): David Avis and Charles Jordan
  • Journal Title: arXiv Volume: 1511:06487 Pages: 1-16
  • Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Comparative computational results for some vertex and facet enumeration codes (2015)
  • Author(s): David Avis and Charles Jordan
  • Journal Title: arXiv Volume: 1510.02545 Pages: 1-4
  • Int'l Joint Research / Acknowledgement Compliant
• [Presentation] Non-CNF QBF Solving with QCIR (2016)
  • Author(s): Charles Jordan, Will Klieber and Martina Seidl
  • Organizer: AAAI-16 Workshop on Beyond NP
  • Place of Presentation: Phoenix (USA)
  • Year and Date: 2016-02-12
  • Int'l Joint Research
• [Presentation] Parallel vertex and facet enumeration with mplrs (2016)
  • Author(s): Skip Jordan
  • Organizer: Algebraic Statistics and Symbolic Computation, Polyhedral Computations Session
  • Place of Presentation: 京都大学（京都市）
  • Invited
• [Presentation] QBFソルバを用いた一般化三並べの拡張の勝敗判定 (2015)
  • Author(s): ディプタラマ, 石黒 裕也, 成澤 和志, 篠原 歩, ジョーダン チャールズ
  • Organizer: ゲームプログラミングワークショップ2015
  • Place of Presentation: 軽井沢学習研修所（長野県）
  • Year and Date: 2015-11-06
• [Remarks] 私のホームページで、論文のPDFなどがあります。
  • URL: https://www-alg.ist.hokudai.ac.jp/~skip/
• [Remarks] lrslibのホームページ。共同研究で作った分散mplrsがあります。
  • URL: http://cgm.cs.mcgill.ca/~avis/C/lrs.html
• [Remarks] 共同研究で作ったmtsという並列逆探索のチュートリアル。
  • URL: http://cgm.cs.mcgill.ca/~avis/doc/tutorial.html
• [Remarks] ホームページ
  • URL: https://www-alg.ist.hokudai.ac.jp/~skip/