| 研究課題/領域番号 |
25730042
|
|---|
| 研究種目 |
若手研究(B)
|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
宋 剛秀 神戸大学, 学内共同利用施設等, 助教 (00625121)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | SAT技術 / 制約プログラミング / 動的制約 / ドメイン特化言語 / ハミルトン閉路問題 / 推論技術 / 国際情報交換 / フランス |
|---|
| 研究概要 |
近年，命題論理式の充足可能性判定 (SAT) 問題を解くためのSAT技術が大きく発展を遂げており，その拡張と応用に注目が集まっている．本研究の目的は，制約の追加・削除に対応したSAT型制約プログラミングシステムを研究開発することにより，既存のSAT技術では困難あるいは不可能だった代謝パスウェイおよびそれを動的に制御する遺伝子調節ネットワークの複合モデルを解析することである．
平成25年度は動的な制約の追加・削除を行うことが可能なSAT型制約プログラミングシステムであるScarabの研究開発を行い，その応用を進めた．Scarabは制約プログラミングのためのドメイン特化言語 (DSL) であるScarab DSL，SAT符号化モジュール，そしてバックエンドのSATソルバーへのインターフェースから構成される．SAT型システム開発者はScarab DSLを用いることで様々な問題を柔軟に制約モデル化可能になる．またScarabはSAT, Max-SAT, 擬似ブール制約など命題論理およびその拡張における推論技術のライブラリであるSat4jと密に結合されており，Java 仮想マシン上で連携して動作することが可能である．
Scarabの基本性能を評価するためにScarabを用いたハミルトン閉路問題のインクリメンタル解法の研究を進め，従来方法と比較して高速な解法システムを実現することに成功した．
これまでSAT技術を応用したシステムは数多く提案されてきたが，Scarabのように制約プログラミングのためのDSLを備えて，Java仮想マシン上でSATソルバーと連携しながら実行できるシステムは少ない．Scarab開発には進歩を続けるSAT技術の応用基盤の提供という意義が存在する．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究における研究課題は大きく分けて次の3つである: (A) パスウェイの制約モデル, (B) 求解システム, (C) 評価と成果物公開. 平成25年度は (B) の求解システムの開発を行い，SAT型制約プログラミングシステムである Scarab を実現し性能を確認した．このことから研究は順調に進行していると考えている．
|
| 今後の研究の推進方策 |
本研究における研究課題は大きく分けて次の3つである: (A) パスウェイの制約モデル, (B) 求解システム, (C) 評価と成果物公開. 平成25年度は (B) の求解システムの開発を行い，SAT型制約プログラミングシステムである Scarab を実現し性能を確認した．平成26年度は (A) のパスウェイの制約モデルに取り組む予定である．この課題に取り組む中で Scarab に機能や性能についての不足がある場合には適宜改善を行う予定である．
|
