Problem Solving with SAT Oracles
| Project/Area Number |
19H04175
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 61030:Intelligent informatics-related
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
Koshimura Miyuki 九州大学, システム情報科学研究院, 助教 (30274492)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
藤田 博 九州大学, システム情報科学研究院, 准教授 (70284552)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥9,750,000 (Direct Cost: ¥7,500,000、Indirect Cost: ¥2,250,000)
Fiscal Year 2022: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
Fiscal Year 2021: ¥2,730,000 (Direct Cost: ¥2,100,000、Indirect Cost: ¥630,000)
Fiscal Year 2020: ¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
Fiscal Year 2019: ¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
|
|---|
| Keywords | 組合せ最適化 / 極小修正集合 / クリーク分割問題 / 実時間スケジューリング / 自動倉庫のスケジューリング / Robust MaxSAT / スケジューリング / 提携構造形成問題 / SAT解法 / SATオラクル / 推移律のSAT符号化 / 極小修正集合の列挙問題 / 擬似ブール制約 / Minimal Correction Set |
|---|
| Outline of Research at the Start |
本研究ではSATオラクル解法の性能向上を目指し、オラクル間の連携や探索ヒューリスティックスなどの技術課題を洗い出し、その解決を図る。また、いくつかの応用問題を通して、その効果を実証する。このため、「SAT/MaxSAT/PBソルバーの開発」、「極小修正集合の列挙」、「MaxSAT/PBソルバーの応用開発」の研究を進める。最後の応用開発では、実時間スケジューリング、提携構造形成問題などに取り組む。
|
| Outline of Final Research Achievements |
We have investigated the SAT oracle method, which uses the SAT solver call as NP oracle, by applying it to several applications including (1) enumerating minimal correction subsets (MCSes), (2)clique partitioning problems (3) optimal scheduling in overloaded real-time systems, and (4) optimal scheduling for vertical transport machine in automatic warehouse.
(1) shows that our proposed method is more efficient that state-of-the-art MCS enumerators on average to deal with partial MaxSAT instances. (2) introduces a series of concise Integer Linear Programming formulations that can reduce even more transitivity constraints, and theoretically evaluates the amount of reduction. (3) demonstrate that, compared with the existing satisfiability-based methods, the proposed method significantly improves the efficiency of identifying the optimal schedule. (4) shows that the proposed method can solve the practical problems in reasonable time, and succeeds to improve transport capacity.
|
| Academic Significance and Societal Importance of the Research Achievements |
(1)から(4)のいずれも手法でも有効性が確認できた。これは、SATオラクル解法の能力の高さを示している。特に、(2)は推移律というかなり一般的な制約についてその数の削減手法を提案しており、その恩恵を享受できる適用分野は広く学術的意義は高い。
(4)で用いられているのは、SAT分野の基礎的な符号化技術ではあるが、物流分野の重要な技術的課題である自動倉庫の高速化と省スペース化に貢献する成果であり、社会的意義は大きい。
|
Report
(5 results)
Research Products
(19 results)
