2012 Fiscal Year Annual Research Report
命題論理の推論技術を用いた高性能かつ柔軟な制約プログラミングシステムの実現
| Project/Area Number |
24300007
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Research Institution | Kobe University |
|---|
Principal Investigator |
田村 直之 神戸大学, 情報基盤センター, 教授 (60207248)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
番原 睦則 神戸大学, 情報基盤センター, 准教授 (80290774)
宋 剛秀 神戸大学, 情報基盤センター, 助教 (00625121)
井上 克巳 国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321)
鍋島 英知 山梨大学, 医学工学総合研究部, 准教授 (10334848)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | 制約プログラミング / 充足可能性判定問題 / 命題論理 |
|---|
| Research Abstract |
命題論理の推論技術を用いた高性能かつ柔軟な制約プログラミングシステムの実現に関する研究開発を行い,18件の学会誌論文・国際会議論文の公表,14件の学会発表を行った.また,設定した各研究テーマに関しては以下の研究開発成果を得た.
A.フレキシブル制約に関する研究開発:フレキシブル制約の一種である重み付きソフト制約についていて,それらを擬似ブール制約に一旦符号化し,さらに命題論理の充足可能性判定問題(SAT)に符号化する方法について研究開発を行った.特に擬似ブール制約をSAT符号化するシステムとしてPBSugarを開発した.また,多目的制約最適化問題に関する研究を行った.
B.動的な制約変更に関する研究開発 : 制約充足問題(CSP)をSATに符号化し求解するシステムとしてCoprisおよびScarabを開発し,それらのシステム上で動的に制約変更を可能にする方法について研究開発を行った.また,本研究チームで開発しているGlueMiniSatについて,求解中に動的に制約を簡単化する軽量な手法について検討し,評価を行った.
C.ドメイン拡張に関する研究開発:多倍長整数をSAT符号化できるシステムとしてAzucarの研究開発を行った.また記号ドメインへの拡張として解集合プログラミング(ASP)に着目し,ASP上での制約記述とその符号化について研究を開始した.
D.応用研究開発 : システム生物学への応用として,遺伝子制御やシグナル伝達のネットワークの離散モデルであるブーリアンネットワークを取り上げ,論理プログラミング意味論による動的遷移およびアトラクターの解析を行った.また,時間割問題への応用研究を開始した.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画で設定した各研究テーマに関し研究開発を進め,18件の学会誌論文・国際会議論文の公表,14件の学会発表を行った.また,GlueMiniSat, PBSugar, Copris, Scarab, Azucar等のソフトウェアを開発し公開している.以上の点から研究はおおむね順調に進展していると判断した.
|
| Strategy for Future Research Activity |
当初の計画に従い,設定した以下の各研究テーマに関する研究開発を進める.A.フレキシブル制約に関する研究開発:ソフト制約のSAT符号化.B.動的な制約変更に関する研究開発:ScarabとSat4jの連携による動的な制約変更への対応。C.ドメイン拡張に関する研究開発:ASP上の制約プログラミングの実現.D.応用研究開発:システム生物学,時間割問題への応用.
|
| Expenditure Plans for the Next FY Research Funding |
応用研究の問題を実行する計算サーバーの導入を予定していたが,導入しなかった直接経費次年度使用額が生じた.平成25年度に同様の計算サーバーの導入を計画している.
|
Research Products
(33 results)
