• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Problem Solving with SAT Oracles

Research Project

Project/Area Number 19H04175
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Review Section Basic Section 61030:Intelligent informatics-related
Research InstitutionKyushu 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)
  • 2022 Annual Research Report   Final Research Report ( PDF )
  • 2021 Annual Research Report
  • 2020 Annual Research Report
  • 2019 Annual Research Report
  • Research Products

    (19 results)

All 2023 2022 2021 2020 2019

All Journal Article (7 results) (of which Int'l Joint Research: 4 results,  Peer Reviewed: 7 results,  Open Access: 3 results) Presentation (10 results) (of which Int'l Joint Research: 4 results) Patent(Industrial Property Rights) (2 results)

  • [Journal Article] Concise integer linear programming formulation for clique partitioning problems2022

    • Author(s)
      Miyuki Koshimura, Emi Watanabe, Yuko Sakurai, Makoto Yokoo
    • Journal Title

      Constraints

      Volume: 27 Issue: 1-2 Pages: 99-115

    • DOI

      10.1007/s10601-022-09326-z

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Impossibility of weakly stable and strategy-proof mechanism2022

    • Author(s)
      Sung-Ho Cho, Miyuki Koshimura, Pink Mandal, Kentaro Yahiro, Makoto Yokoo
    • Journal Title

      Economics Letters

      Volume: 217 Pages: 1-4

    • DOI

      10.1016/j.econlet.2022.110675

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Robust Weighted Partial Maximum Satisfiability Problem: Challenge to Σ2P-Complete Problem2022

    • Author(s)
      Sugahara Tomoya、Yamashita Kaito、Barrot Nathanael、Koshimura Miyuki、Yokoo Makoto
    • Journal Title

      Pacific Rim International Conference on Artificial Intelligence

      Volume: 1 Pages: 17-31

    • DOI

      10.1007/978-3-031-20862-1_2

    • ISBN
      9783031208614, 9783031208621
    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Modeling and Solving Scheduling in Overloaded Situations with Weighted Partial Ma×SAT2021

    • Author(s)
      Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Rong Huang, Wenxin Yu, Fagen Li
    • Journal Title

      Mathematical Problems in Engineering

      Volume: 2021 Pages: 1-17

    • DOI

      10.1155/2021/9615463

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT2019

    • Author(s)
      Aolong Zha, Miyuki Koshimura, Hiroshi Fujita
    • Journal Title

      Constraints

      Volume: 24 Issue: 2 Pages: 133-161

    • DOI

      10.1007/s10601-018-9299-0

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 分割決定木を用いた分割関数ゲームの提携構造形成アルゴリズム2019

    • Author(s)
      査 澳龍、越村 三幸、櫻井 祐子、横尾 真
    • Journal Title

      電子情報通信学会論文誌D 情報・システム

      Volume: J102-D Pages: 313-323

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A comparative analysis and improvement of MaxSAT encodings for coalition structure generation under MC-nets2019

    • Author(s)
      Xiaojuan Liao、Miyuki Koshimura
    • Journal Title

      Journal of Logic and Computation

      Volume: 29 Issue: 6 Pages: 913-931

    • DOI

      10.1093/logcom/exz017

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Presentation] ラムゼーグラフの二つの遷移2023

    • Author(s)
      越村 三幸、永野 崇
    • Organizer
      2023年電子情報通信学会総合大会
    • Related Report
      2022 Annual Research Report
  • [Presentation] 垂直搬送機のMaxSATによる最適スケジューリング2022

    • Author(s)
      越村 三幸、野田 五十樹
    • Organizer
      スケジューリング・シンポジウム2022
    • Related Report
      2022 Annual Research Report
  • [Presentation] 敵対者が存在する重み付き MaxSAT の定式化と厳密アルゴリズムの提案2022

    • Author(s)
      山下魁人、菅原知地、越村 三幸、横尾真
    • Organizer
      Symposium on Multi Agent Systems for Harmonization 2022 (SMASH22)
    • Related Report
      2021 Annual Research Report
  • [Presentation] ADSAT:敵対者が存在するMaxSAT2021

    • Author(s)
      菅原知地、越村 三幸、横尾 真
    • Organizer
      人工知能学会全国 大会(第35回)
    • Related Report
      2021 Annual Research Report
  • [Presentation] CNF Encodings for the Min-Max Multiple Traveling Salesmen Problem2020

    • Author(s)
      Aolong Zha, Rongxuan Gao, Qiong Chang, Miyuki Koshimura, Itsuki Noda
    • Organizer
      2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI)
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 推移関係を表すSAT節の削減2020

    • Author(s)
      越村 三幸, 廖 暁鵑, 渡部 恵海, 櫻井 祐子, 横尾 真
    • Organizer
      2020年度人工知能学会全国大会
    • Related Report
      2020 Annual Research Report
  • [Presentation] A Simple yet Efficient MCSes Enumeration with SAT Oracles2020

    • Author(s)
      Miyuki Koshimura, Ken Satoh
    • Organizer
      12th Asian Conference on Intelligent Information and Database Systems
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] SATソルバーGlucoseを用いたMCS列挙2019

    • Author(s)
      越村三幸、佐藤健
    • Organizer
      2019年度人工知能学会全国大会
    • Related Report
      2019 Annual Research Report
  • [Presentation] Maximum Satisfiability Formulation for Optimal Scheduling in Overloaded Real-Time Systems2019

    • Author(s)
      Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Rong Huang, Wenxin Yu
    • Organizer
      PRICAI: 16th Pacific Rim International Conference on Artificial Intelligence
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Solving Coalition Structure Generation Problems over Weighted Graph2019

    • Author(s)
      Emi Watanabe, Miyuki Koshimura, Yuko Sakurai, Makoto Yokoo
    • Organizer
      PRIMA 2019: 22nd International Conference on Principles and Practice of Multi-Agent Systems
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Patent(Industrial Property Rights)] 物流倉庫の制御装置、及び物流倉庫の制御方法2022

    • Inventor(s)
      越村、岡本、野田、小出
    • Industrial Property Rights Holder
      越村、岡本、野田、小出
    • Industrial Property Rights Type
      特許
    • Filing Date
      2022
    • Related Report
      2022 Annual Research Report
  • [Patent(Industrial Property Rights)] 物流倉庫の制御装置、及び物流倉庫の制御方法2021

    • Inventor(s)
      越村、野田、加藤
    • Industrial Property Rights Holder
      越村、野田、加藤
    • Industrial Property Rights Type
      特許
    • Filing Date
      2021
    • Related Report
      2021 Annual Research Report

URL: 

Published: 2019-04-18   Modified: 2024-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi