| 研究課題/領域番号 |
22K11973
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
田村 直之 神戸大学, DX・情報統括本部, 名誉教授 (60207248)
|
|---|
| 研究分担者 |
宋 剛秀 神戸大学, 情報基盤センター, 准教授 (00625121)
番原 睦則 名古屋大学, 情報学研究科, 教授 (80290774)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2025-03-31
|
| キーワード | 制約充足問題 / 制約プログラミング / 制約ソルバー / SAT技術 / SATソルバー |
|---|
| 研究実績の概要 |
本研究の目的は，制約充足問題に対する新しいSAT解法技術を研究開発し，さらに開発したシステムを実用的な問題に応用し，既存技術では解けなかった問題の解決を目指すとともに研究開発した技術を評価することである．研究遂行のため(WG1) SAT符号化手法の研究開発，(WG2) SAT型制約ソルバーの研究開発，(WG3) 応用・評価の3つの研究開発テーマを設定し，研究開発を分担して進めている．
(WG1)では，研究代表者らが考案した順序符号化を用いて整数係数を持つ線形制約をSAT符号化した場合に，どのような変数順序で符号化アルゴリズムを実行すると良いかについて実験を行い，結果を評価した．また，接頭和を用いた符号化法，剰余記数法を用いた符号化法，MDDを用いた符号化法について検討を進めた．
(WG2)では，ベースとなるSAT型制約ソルバーFun-sCOPで2022年XCSP3競技会 (http://xcsp.org/competitions/)に参加し，Main CSPトラックで準優勝という結果を得た．
(WG3)では，システム生物学の分野で用いられている非同期多値ネットワークの解析を行うためのSAT型手法を考案し，そのシステムを開発した(雑誌論文1)．具体的には，非同期オートマタネットワークとして表現されている遺伝子ネットワークについて，そのアトラクターをSATソルバーを利用して発見することにより，元の遺伝子ネットワークの定性的な分析を可能にした．次に，複数の車種からなる車を製造する場合に，全体の平均燃費がCAFE規制値を満たす範囲内で総販売予想金額を最大にする組み合わせを探索するための手法を考案し，ASPソルバーを用いたシステムを開発した(雑誌論文2)．さらに，グラフの支配集合や独立集合をSAT型手法で効率良く求める方法について研究を行い結果を学会で発表した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
(WG1) SAT符号化手法の研究開発，(WG2) SAT型制約ソルバーの研究開発，(WG3) 応用・評価の3つの研究開発テーマのそれぞれについて，以下の理由によりおおむね順調に進展していると考えている．
(WG1)では，順序符号化に関する基本的な実験・評価を行い，本質的な問題点がどのような部分に存在するのかを明らかにした．
(WG2)では，研究開発のベースの一つであるSAT型制約ソルバーFun-sCOPについて，国際的な制約ソルバーの競技会に参加し2位になるという良い結果を得た．
(WG3)では，システム生物学など実用的な研究分野のいくつかの問題に対し，SAT型手法を応用し，その有効性を示すことができた．
|
| 今後の研究の推進方策 |
(WG1) SAT符号化手法の研究開発，(WG2) SAT型制約ソルバーの研究開発，(WG3) 応用・評価の3つの研究開発テーマのそれぞれに関し，以下のように今後の研究を推進する予定である．
(WG1)では，接頭和を用いた符号化法，剰余記数法を用いた符号化法，MDDを用いた符号化法の検討をさらに進め，アルゴリズムの実装および実験評価を行う．
(WG2)では，(WG1)で研究開発したSAT符号化手法を既開発のSugar, Copris等に組み込むことで，新しいSAT型制約ソルバーを実現する．
(WG3)では，これまで進めてきた応用分野での研究をさらに進展させるとともに，グラフの支配集合や独立集合の遷移問題への応用を進める．
|
| 次年度使用額が生じた理由 |
2022年度は研究打合せを対面ではなくリモートで実施することが多かったため旅費の使用が少額となった．
2023年度以降は，対面での研究打合せ回数を増やすことで，より深い研究交流を実現し，より良い研究成果の達成を目指す予定である．
|
