| 研究課題/領域番号 |
25730042
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
宋 剛秀 神戸大学, 学内共同利用施設等, 助教 (00625121)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | SAT技術 / 制約プログラミング / 動的制約 / ドメイン特化言語 / ハミルトン閉路問題 / 推論技術 / 国際情報交換 / フランス |
|---|
| 研究実績の概要 |
近年，命題論理式の充足可能性判定 (SAT) 問題を解くためのSAT技術が大きく発展を遂げており，その拡張と応用に注目が集まっている．本研究の目的は，制約の追加・削除に対応したSAT型制約プログラミングシステムを研究開発することにより，既存のSAT技術では困難あるいは不可能だった代謝パスウェイおよびそれを動的に制御する遺伝子調節ネットワークの複合モデルを解析することである．
平成26年度は動的な制約の追加・削除を行うことが可能なSAT型制約プログラミングシステムであるScarabについて機能拡張を行った．具体的には組み込み制約の利用や非充足コアの計算が可能になった．この機能拡張の内容の一部については日本ソフトウェア科学会第31回大会で口頭発表を行った (高橋奨励賞受賞).
また制約プログラミングに関連して制約解集合プログラミングシステム muffin を日本ソフトウェア科学会第31回大会で口頭発表し，web page で公開した．この他に Scarab を利用したハミルトン閉路ソルバー hss を開発して web page に公開し，論文発表を The 14th European Conference on Logics in Artificial Intelligence (JELIA 2014) で行った．
これまでSAT技術を応用したシステムは数多く提案されてきたが，Scarabのように制約プログラミングのためのDSLを備えて，Java仮想マシン上でSATソルバーと連携しながら実行できるシステムは少ない．Scarab開発には進歩を続けるSAT技術の応用基盤の提供という意義が存在する．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究における研究課題は大きく分けて次の3つである: (A) パスウェイの制約モデル, (B) 求解システム, (C) 評価と成果物公開. 平成26年度は (B) の求解システムの開発を継続して行い，また開発したScarabおよびその応用を (C) 口頭発表・論文発表・インターネットを通じて公開・成果発表した．このことから研究は順調に進行していると考えている．
|
| 今後の研究の推進方策 |
本研究における研究課題は大きく分けて次の3つである: (A) パスウェイの制約モデル, (B) 求解システム, (C) 評価と成果物公開.平成26年度は (B) の求解システムの開発, (C) 評価と成果物公開を行った．
平成27年度は引き続き (B), (C) と共に (A) のパスウェイの制約モデルに取り組む予定である．
また，この課題に取り組む中で Scarab に機能や性能についての不足がある場合には適宜改善を行う予定である
|
| 備考 |
本研究プロジェクトで開発している (1) SAT型制約プログラミングシステム Scarab，それを基にした (2) ハミルトン閉路ソルバー hss, (3) 制約解集合プログラミングシステム muffin の公開 web page
|
