2020 Fiscal Year Annual Research Report
Problem Solving with SAT Oracles
| Project/Area Number |
19H04175
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
越村 三幸 九州大学, システム情報科学研究院, 助教 (30274492)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | 実時間スケジューリング / 推移律のSAT符号化 |
|---|
| Outline of Annual Research Achievements |
本年度は、SATオラクルを用いた解法に関して、（A）実時間システムの最適スケジューリング、（B）推移関係を表すSAT節の削減手法、（C）Robust MaxSATの実装、に取り組み、２件の学術発表を行った。
（Aa）過負荷な単一プロセッサの実時間スケジューリング問題のMaxSAT解法に関する論文を執筆した。
（Ab）物流センター内の仕分け機の最適スケジューリングの為のMaxSAT解法のプロトタイプを作成した。
（B）グラフの頂点間の到達可能性を判定する為のSAT節の数を削減する新たな手法を編み出し、従来手法に比べ効果があることを定量的に確かめた。
（C）従来の実装の見直しを行い、数倍程度の速度向上に成功した。
|
| 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）については従来の削減手法より優れた手法の着想を得た。平均をとって、上記のような区分を選択した。
|
| Strategy for Future Research Activity |
（Ab）プロトタイプの実験結果を踏まえ、実時間スケジューリングへの拡張を図る。
（B）新削減手法の理論的及び実験的評価を行う。
（C）QBF（Quantified Boolean Formula）ソルバーの実装法を参考に、Robust MaxSATソルバーの性能向上を図る。
|
