| 研究課題/領域番号 |
22K11973
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
田村 直之 神戸大学, DX・情報統括本部, 名誉教授 (60207248)
|
|---|
| 研究分担者 |
宋 剛秀 神戸大学, 情報基盤センター, 准教授 (00625121)
番原 睦則 名古屋大学, 情報学研究科, 教授 (80290774)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2022年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2024年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2023年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2022年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 制約充足問題 / 制約プログラミング / 制約ソルバー / SAT技術 / SATソルバー / 充足可能性問題 |
|---|
| 研究開始時の研究の概要 |
制約充足問題 (以下，CSP)は複数の条件(制約)の組合せからなる問題であり，制約ソルバーは与えられたCSPの解を探索するシステムである．制約プログラミングシステムは，処理系に制約ソルバーを組込むことで，解法プログラムを記述することなく高度な問題解決を可能にする宣言的プログラミングシステムの一種である．
一方，命題論理の充足可能性問題 (以下，SAT)を解くSATソルバーの性能は2000年以降に飛躍的に向上し，これまでは到底不可能だと思われていた規模の問題を解くことができるようになった．
本研究では，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)では，これまで進めてきた応用分野での研究をさらに進展させるとともに，グラフの支配集合や独立集合の遷移問題への応用を進める．
|
