2021 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 | Robust MaxSAT / スケジューリング |
|---|
| Outline of Annual Research Achievements |
本年度も昨年度に引き続き、(A)実時間システムの最適スケジューリング、(B)推移関係を表すSAT節の削減手法、(C)Robust MaxSATの実装、に取り組み、３件の学術発表を行った。また、当初計画にはなかった(D)実用的解法アルゴリズムの開発のための演算不変性に関する計算機実験をSATを技術を利用して行った。
(A) 物流センター内の仕分け機のMaxSAT技術を利用した最適化スケジューリングの（荷物の戻り動作、入口階と目的階が一致している荷物の連続搬入ができるように）拡張を行い、実機の動きにより適したスケジューリングができるようにした。そして、搬送能力が向上することを確かめた。また、プロトタイプを特許出願した。
(B) 推移律を表現するSAT節の削減の手法を線形整数最適化問題(ILP)による解法にも適用した。クリーク分割問題（CPP:clique partitioning problem）を対象にしたILPにおける最新手法より削減率の点で優れていることを理論的に示し、最新のILPソルバーを使った実験でもその優位性を確かめた。
(C) 昨年度開発した解法が、QBF(Quantified Boolean Formula)ソルバーを使った手法に比べても優れていることをランダムインスタンスとCPPのインスタンスを使った実験により確かめた。
(D) 具体的な方程式をいくつか考え、定義域を狭めた問題設定で３項演算の不変演算数を全て列挙することに成功した。
|
| 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 |
(A) 実機での性能評価を行い、従来手法と比較を行う。
(B) 成果をトップジャーナル（制約充足関連）に投稿する。
(C) 成果の国際会議への投稿を目指す。
|
