Problem Solving with SAT Oracles

2022 Fiscal Year Final Research Report

• 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
• Keywords: 組合せ最適化 / 極小修正集合 / クリーク分割問題 / 実時間スケジューリング / 自動倉庫のスケジューリング

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.

Free Research Field

知能情報学

Academic Significance and Societal Importance of the Research Achievements

(1)から(4)のいずれも手法でも有効性が確認できた。これは、SATオラクル解法の能力の高さを示している。特に、(2)は推移律というかなり一般的な制約についてその数の削減手法を提案しており、その恩恵を享受できる適用分野は広く学術的意義は高い。
(4)で用いられているのは、SAT分野の基礎的な符号化技術ではあるが、物流分野の重要な技術的課題である自動倉庫の高速化と省スペース化に貢献する成果であり、社会的意義は大きい。