2019 Fiscal Year Annual Research Report
Problem Solving with SAT Oracles
| Project/Area Number |
19H04175
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
越村 三幸 九州大学, システム情報科学研究院, 助教 (30274492)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
藤田 博 九州大学, システム情報科学研究院, 准教授 (70284552)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | 極小修正集合 / 提携構造形成問題 / 実時間スケジューリング / 擬似ブール制約 |
|---|
| Outline of Annual Research Achievements |
本年度は、SATオラクルを用いた（A）極小修正集合（MCS）の列挙問題、（B）提携構造形成問題（CSG)、（C）実時間システムの最適スケジューリング問題、（D）擬似ブール（PB）制約のSAT符号化、に取り組み、７件の学術発表（内３件は学術誌）を行った。
（A）過剰制約問題のMCSを列挙する簡便な手法を考案し、その実装が最新のシステムとほぼ同程度の性能を示すことを確認した。特に、ソフト制約とハード制約が混在する問題では、世界最高性能を示すことができた。
（B）MC-nets、分割決定木、重み付きグラフ、で表現されたCSGについて、MaxSATを用いた解法を考案し、良好な性能を示すことを確かめた。また、重み付きグラフでは、整数計画法による解法より良好な結果が得られた。
（C）過負荷な単一プロセッサの実時間スケジューリング問題のMaxSAT解法を考案し、従来のSMTを用いた解法に比べ、格段に高い性能を達成した。
（D）PB制約のSAT符号化を、多段階に剰余計算を適用することにより行う手法を考案し、最新のSATソルバーで効率的に処理できることを確かめた。
研究協力者とは、メールや研究集会での研究交流を通じて意見交換等している。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
（B）については当初の計画以上に進展、（A）（C）（D）については概ね順調に進展しているが、当初計画していたSATソルバーの研究開発にはあまり進展がなかった。平均をとって、上記のような区分を選択した。
|
| Strategy for Future Research Activity |
（A）学会での研究交流により指摘されている現解法の問題点を整理し、さらなる性能向上を目指す。
（B）CSGの数理的解法における推移律の取り扱いについて、重点的に取り組む。
（C）新たに荷物仕分け機の最適化スケジューリング問題に取り組む。
（D）PB制約の応用について検討する。
|
