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

2014 年度 実績報告書

近似手法と数式処理の融合による実数多項式制約の効率化

研究課題

研究課題/領域番号 23300005
研究機関北陸先端科学技術大学院大学

研究代表者

小川 瑞史  北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)

研究分担者 廣川 直  北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
関 浩之  名古屋大学, 情報科学研究科, 教授 (80196948)
研究期間 (年度) 2011-04-01 – 2015-03-31
キーワードSMTソルバ / 多項式制約 / 充足性判定
研究実績の概要

H26年度は、実数上の多項式制約の充足性判定器(SMTソルバ)raSATの実装を主に学生雇用により進め、SMTcomp 2014(ウィーン数理論理連合国際会議 H26年7月に共催)に参加し、またSMTワークショップ(同共催)において口頭発表を行った。raSATの実装における主たる進捗は、(1) 効率化のための有効な戦略の発見と多岐にわたる実験による実証、(2) H25年度までは主に不等式制約のみが対象であったが、(複数)等式制約への拡張を中間値の定理を用いた拡張による実装、の二点である。(1)については、H25年度まで、有効と考えていた探索戦略が実際にはランダムな選択と有意な差がないことが実験によりわかり、探索先着の再設計を余儀なくされたが、幸いにして新たな探索戦略およびその有効性の検証を実験を通して行うことができた。(2) については、まだ十分な効率化は進めていないが、ベンチマークにより、良好な実験結果が示された。また、ロレーヌ大学LORIA のPascal Fontain博士の開発するSMTフレームワーク VeriT 上での再実装による融合を今後進める予定である。(これは11月に2週間 LORIA に滞在して討論し、合意に達した。)
H26年度は、DSMT-comp への初挑戦は参加システム4件中4位と成績は振るわなかったが、H27年度以降も挑戦する予定である。現状では Microsoft research による defacto standard なSMTソルバZ3 に及ばないが、かなりせまる性能を示しており(一部のベンチマークでは上回る)、上位の入賞をめざす。また、難関国際会議である、第21回システム構成・解析のためのツールとアルゴリズム国際会議 (TACAS 2015) には不採択となったが、現在,第10回システム構成のフロンティア国際会議 (FroCos 2015)への再投稿を準備中である。

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

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

今後の研究の推進方策

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

  • 研究成果

    (2件)

すべて 2014 その他

すべて 学会発表 (1件) 備考 (1件)

  • [学会発表] raSAT: SMT for Polynomial Inequality(口頭発表)2014

    • 著者名/発表者名
      To Van Khanh, Mizuhito Ogawa
    • 学会等名
      第12回SMTワークショップ(SMT 2014)
    • 発表場所
      ウィーン、オーストリア
    • 年月日
      2014-07-17 – 2014-07-18
  • [備考] raSAT

    • URL

      http://www.jaist.ac.jp/~mizuhito/tools/rasat.html

URL: 

公開日: 2016-06-01  

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

Powered by NII kakenhi