2023 Fiscal Year Research-status Report
Research and Development of a New SAT Solving Technologies for Constraint Satisfaction Problems
| Project/Area Number |
22K11973
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
田村 直之 神戸大学, DX・情報統括本部, 名誉教授 (60207248)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
宋 剛秀 神戸大学, 情報基盤センター, 准教授 (00625121)
番原 睦則 名古屋大学, 情報学研究科, 教授 (80290774)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Keywords | 制約充足問題 / 制約プログラミング / 制約ソルバー / SAT技術 / SATソルバー |
|---|
| Outline of Annual Research Achievements |
本研究の目的は，制約充足問題に対する新しいSAT解法技術を研究開発し，さらに開発したシステムを実用的な問題に応用し，既存技術では解けなかった問題の解決を目指すとともに研究開発した技術を評価することである．研究遂行のため(WG1) SAT符号化手法の研究開発，(WG2) SAT型制約ソルバーの研究開発，(WG3) 応用・評価の3つの研究開発テーマを設定し，研究開発を分担して進めている．
(WG1)では，昨年度に引き続き順序符号化に関する実験を行い，結果を評価した．また，接頭和を用いた符号化法，剰余記数法を用いた符号化法，MDDを用いた符号化法について検討を進めた．
(WG2)では，ベースとなるSAT型制約ソルバーFun-sCOPで2023年XCSP3競技会 (http://xcsp.org/competitions/)に参加し，昨年度と同様にMain CSPトラックで準優勝という結果を得た．また，Python上で動作するSAT型制約ソルバーのプロトタイプを開発した．
(WG3)では，非同期オートマタネットワークとして表現されている遺伝子ネットワークについて，そのアトラクターをSATソルバーを利用して発見する手法の発展研究を行い，成果を(雑誌論文3)で発表した．また(雑誌論文1)で，供給経路と電流・電圧に関する制約を満たす配電網の構成を求める配電網問題，および配電網問題の2つの実行可能解が与えられたとき，遷移制約を満たしつつ一方の解から他方の解へ到達できるかを判定する配電網遷移問題について研究成果を発表した．さらに(雑誌論文2)で，与えられたグラフの2つのハミルトン閉路が与えられたとき，定められた遷移制約を満たしながら一方の閉路から他方の閉路に遷移することが可能かどうかを判定するハミルトン閉路遷移問題について研究成果を発表した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
(WG1) SAT符号化手法の研究開発，(WG2) SAT型制約ソルバーの研究開発，(WG3) 応用・評価の3つの研究開発テーマのそれぞれについて，以下の理由によりおおむね順調に進展していると考えている．
(WG1)では，順序符号化に関する基本的な実験・評価を進め，問題点の解決方法について検討した．
(WG2)では，研究開発のベースの一つであるSAT型制約ソルバーFun-sCOPについて，昨年度に引き続き国際的な制約ソルバーの競技会に参加し2位になるという良い結果を得た．
(WG3)では，システム生物学，配電網遷移問題，ハミルトン閉路遷移問題など実用的な研究分野のいくつかの問題に対し，SAT型手法を応用し，その有効性を示すことができた．
|
| Strategy for Future Research Activity |
(WG1) SAT符号化手法の研究開発，(WG2) SAT型制約ソルバーの研究開発，(WG3) 応用・評価の3つの研究開発テーマのそれぞれに関し，以下のように今後の研究を推進する予定である．
(WG1)では，接頭和を用いた符号化法，剰余記数法を用いた符号化法，MDDを用いた符号化法の検討をさらに進め，アルゴリズムの実装および実験評価を行う．
(WG2)では，(WG1)で研究開発したSAT符号化手法を既開発のSugar, Copris等に組み込むことで，新しいSAT型制約ソルバーを実現する．また，Python上に実装したプロトタイプを完成させる．
(WG3)では，これまで進めてきた応用分野での研究をさらに進展させるとともに，グラフの支配集合や独立集合の遷移問題への応用を進める．
|
| Causes of Carryover |
2023年度は2022年度からの繰越しがあったため，その一部がさらに次年度使用となった．
2024年度は成果発表回数などを調整し研究費を使用する予定である．
|
