| 研究課題/領域番号 |
23300005
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
|
|---|
| 研究分担者 |
廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
関 浩之 名古屋大学, 情報科学研究科, 教授 (80196948)
|
|---|
| 研究期間 (年度) |
2011-04-01 – 2015-03-31
|
| キーワード | ソフトウェア / 仕様記述 / 仕様検証 / 制約解消 / 数式処理 |
|---|
| 研究概要 |
実数多項式制約解消の効率化において、1.実数多項式不等式の制約を解くSMTの設計・実装（北陸先端大・小川）、2.数式処理に基づく実数多項式制約の厳密解を与えるQE-CADアルゴリズムの持ち上げ段階への書換え手法の応用の検討（北陸先端大・廣川）、3.量的情報流解析への応用の検討（奈良先端大・関）を進めた。
1 は、実数上の多項式制約解消について、当初多項式不等式に制限により、raSATループという単純かつ有効な詳細化手法を提案した。新たな区間演算法の提案や実用的効率向上のため戦略の導入により、raSAT の初期実装は SMT-compのベンチマーク群の不等式問題で最新の SMT Z3 4.3 (Microsoft reseach)に比較可能なレベルの性能を示している。現在、実装の64bit化ならびに浮動小数点演算に起因する健全性違反に対するiRRAMパッケージによる確認ステップなどの実装を行い、プロトタイプを公開した。(http://www.jaist.ac.jp/~mizuhito/tools/rasat.html)
2. は、項書換え系の完備化手法のGroebner基底計算への直接的応用を検討したが、項書換え系における効率化のポイントとGroebner基底のポイントが異なることが判明し、再検討を進める。
3. は、連続値となる量的情報流の前段階として、離散値の場合のXMLデータベースの質問処理における確定依存性の決定可能性、ならびにスキーマ変換の際の質問応答性の（強・弱）等価保存判定の計算量について研究を進めた。木変換器T1,T2で表されるXML質問処理において T2がT1に確定依存とは、部分関数f が存在して、f・T1 = T2 となることをいう。線形上昇型木変換器では確定依存性の決定可能性、およびその計算量を示した（論文誌1件、査読付国際会議1件）
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初は、区間演算を用いる近似手法と数式処理QE-CADアルゴリズムとの融合を図る計画であったが、現在、近似的手法による多項式不等式処理、代数的手法（Groebner基底など）による多項式等式処理を組み合わせた、QE-CADアルゴリズムとは異なるアプローチによる実用的効率化の可能性が見えており、当初計画以上のインパクトの可能性を示している。
また当初予定に比べ、ツール実装・開発に重点をおいており、64bit化、浮動小数点演算に起因する健全性違反に対する誤差上限が保証されるiRRAMパッケージの利用などを進め、プロトタイプ公開にいたり、現在 SMT-Comp 2014 (SMTソルバの競技会）への参加を準備している。論文発表については、ハイレベルな国際会議 (ASE2013, IJCAR2014)に投稿し、残念ながら不採録となったが、インフォーマルな機会である SMT workshop 2014 に投稿中であり、同分野の海外研究者からコメントを頂き、再投稿の準備を進める。
|
| 今後の研究の推進方策 |
今後の進め方は、4点からなる。(1) ツールraSAT開発のため研究員雇用していた博士後期課程学生の修了に伴い、新たな博士前期課程学生1名の研究員雇用。(2) SMT-Comp 2014 への参加、(3) 論文再投稿の前に、海外同分野研究者によるコメントをいただくために SMT workshop 2014 にて発表し、本年度後期にトップランクの国際会議および国際論文誌に投稿を行う。(4) 多項式等式制約のため、中間値の定理に基づく手法の実装、さらにGroebner基底など数式手法の一部を取り入れ実装を行う。
さらに研究分担者やベトナム国家大学、ナンシー大学LORIAなどと共同した丸め誤差解析やバイナリ解析などへの応用も並行して進める。
|
