• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

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

公募研究

研究領域多面的アプローチの統合による計算限界の解明
研究課題/領域番号 15H00847
研究種目

新学術領域研究(研究領域提案型)

配分区分補助金
審査区分 理工系
研究機関北海道大学

研究代表者

ジョーダン チャールズハロルド  北海道大学, 情報科学研究科, 助教 (60647577)

研究期間 (年度) 2015-04-01 – 2017-03-31
研究課題ステータス 完了 (2016年度)
配分額 *注記
4,940千円 (直接経費: 3,800千円、間接経費: 1,140千円)
2016年度: 2,470千円 (直接経費: 1,900千円、間接経費: 570千円)
2015年度: 2,470千円 (直接経費: 1,900千円、間接経費: 570千円)
キーワード記述計算量 / 並列計算 / 分散計算 / 機械学習 / 知識発見 / 機会学習
研究実績の概要

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

現在までの達成度 (段落)

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

今後の研究の推進方策

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

報告書

(2件)
  • 2016 実績報告書
  • 2015 実績報告書
  • 研究成果

    (13件)

すべて 2016 2015 その他

すべて 雑誌論文 (6件) (うち国際共著 5件、 査読あり 2件、 オープンアクセス 2件、 謝辞記載あり 6件) 学会発表 (3件) (うち国際学会 1件、 招待講演 1件) 備考 (4件)

  • [雑誌論文] The Kahr-Moore-Wang Class Contains Untestable Properties2016

    • 著者名/発表者名
      Charles Jordan and Thomas Zeugmann
    • 雑誌名

      Baltic Journal of Modern Computing

      巻: 4 号: 4 ページ: 736-752

    • DOI

      10.22364/bjmc.2016.4.4.11

    • 関連する報告書
      2016 実績報告書
    • 査読あり / オープンアクセス / 国際共著 / 謝辞記載あり
  • [雑誌論文] A parallel framework for reverse search using mts2016

    • 著者名/発表者名
      David Avis and Charles Jordan
    • 雑誌名

      arXiv:1610.07735

      巻: なし

    • 関連する報告書
      2016 実績報告書
    • 謝辞記載あり
  • [雑誌論文] Machine Learning with Guarantees using Descriptive Complexity and SMT Solvers2016

    • 著者名/発表者名
      Charles Jordan and Lukasz Kaiser
    • 雑誌名

      arXiv:1609.02664

      巻: なし

    • 関連する報告書
      2016 実績報告書
    • 国際共著 / 謝辞記載あり
  • [雑誌論文] QBF Gallery 2014: The QBF Competition at the FLoC 2014 Olympic Games2016

    • 著者名/発表者名
      Mikolas Janota, Charles Jordan, Will Klieber, Florian Lonsing, Martina Seidl and Allen Van Gelder
    • 雑誌名

      Journal on Satisfiability, Boolean Modeling and Computation

      巻: 9 ページ: 187-206

    • 関連する報告書
      2015 実績報告書
    • 査読あり / オープンアクセス / 国際共著 / 謝辞記載あり
  • [雑誌論文] mplrs: A scalable parallel vertex/facet enumeration code2015

    • 著者名/発表者名
      David Avis and Charles Jordan
    • 雑誌名

      arXiv

      巻: 1511:06487 ページ: 1-16

    • 関連する報告書
      2015 実績報告書
    • 国際共著 / 謝辞記載あり
  • [雑誌論文] Comparative computational results for some vertex and facet enumeration codes2015

    • 著者名/発表者名
      David Avis and Charles Jordan
    • 雑誌名

      arXiv

      巻: 1510.02545 ページ: 1-4

    • 関連する報告書
      2015 実績報告書
    • 国際共著 / 謝辞記載あり
  • [学会発表] Non-CNF QBF Solving with QCIR2016

    • 著者名/発表者名
      Charles Jordan, Will Klieber and Martina Seidl
    • 学会等名
      AAAI-16 Workshop on Beyond NP
    • 発表場所
      Phoenix (USA)
    • 年月日
      2016-02-12
    • 関連する報告書
      2015 実績報告書
    • 国際学会
  • [学会発表] Parallel vertex and facet enumeration with mplrs2016

    • 著者名/発表者名
      Skip Jordan
    • 学会等名
      Algebraic Statistics and Symbolic Computation, Polyhedral Computations Session
    • 発表場所
      京都大学(京都市)
    • 関連する報告書
      2016 実績報告書
    • 招待講演
  • [学会発表] QBFソルバを用いた一般化三並べの拡張の勝敗判定2015

    • 著者名/発表者名
      ディプタラマ, 石黒 裕也, 成澤 和志, 篠原 歩, ジョーダン チャールズ
    • 学会等名
      ゲームプログラミングワークショップ2015
    • 発表場所
      軽井沢学習研修所(長野県)
    • 年月日
      2015-11-06
    • 関連する報告書
      2015 実績報告書
  • [備考] 私のホームページで、論文のPDFなどがあります。

    • URL

      https://www-alg.ist.hokudai.ac.jp/~skip/

    • 関連する報告書
      2016 実績報告書
  • [備考] lrslibのホームページ。共同研究で作った分散mplrsがあります。

    • URL

      http://cgm.cs.mcgill.ca/~avis/C/lrs.html

    • 関連する報告書
      2016 実績報告書
  • [備考] 共同研究で作ったmtsという並列逆探索のチュートリアル。

    • URL

      http://cgm.cs.mcgill.ca/~avis/doc/tutorial.html

    • 関連する報告書
      2016 実績報告書
  • [備考] ホームページ

    • URL

      https://www-alg.ist.hokudai.ac.jp/~skip/

    • 関連する報告書
      2015 実績報告書

URL: 

公開日: 2015-04-16   更新日: 2018-03-28  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi