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

Speeding-up SAT-based Constraint Optimization Solvers

Research Project

Project/Area Number 23K11047
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Review Section Basic Section 60050:Software-related
Research InstitutionKobe University

Principal Investigator

宋 剛秀  神戸大学, DX・情報統括本部, 准教授 (00625121)

Project Period (FY) 2023-04-01 – 2027-03-31
Project Status Granted (Fiscal Year 2023)
Budget Amount *help
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2026: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2025: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2024: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2023: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
KeywordsSATソルバー / SAT符号化 / 制約最適化問題 / 制約充足問題 / 制約プログラミング / SATソルバー
Outline of Research at the Start

近年,SAT問題を解くプログラムであるSATソルバーの性能が飛躍的に向上している.
本研究の目的は, SATソルバーを用いた高速なSAT型COPソルバーを実現することである.
そのために2つの方法を研究する.1つは,目的関数を表す線形比較制約の MDD を用いた表現とその符号化方法である. もう1つの方法は極小モデル生成を用いた新しい最適化方法である.
COPソルバーはスケジューリング問題,パッキング問題,時間割問題, クラウド上のソフトウェア要素最適配置問題等の組合せ最適化問題に使われるなど実用性が高く, 高速なSAT型COPソルバーを実現できれば産業分野への応用も期待できる.

Outline of Annual Research Achievements

近年, SAT問題を解くプログラムであるSATソルバーの飛躍的な進歩にともない, 制約充足問題 (CSP) をSAT問題に符号化(SAT符号化)して解くSAT型CSPソルバーが成功している. 本研究では,対象を CSP から制約最適化問題 (COP) へ発展させる.
本研究の目的は, SATソルバーを用いた高速なSAT型COPソルバーを実現することである. そのために2つの方法を研究する.1つは,目的関数を表す線形比較制約の MDD (Multi‐valued Decision Diagram) を用いた表現とその符号化方法である.もう1つの方法は極小モデル生成を用いた新しい最適化方法である.
具体的な研究課題は4つある.(A) MDD を用いた線形比較制約の符号化の研究開発, (B) 極小モデル生成の研究開発, (C) 提案方法を用いたSAT型COPソルバーの実装, (D) 提案SAT型COPソルバーの特長的なアプリケーションの研究開発. それぞれの研究課題は密接に関係しているため逐次的に進めるのではなく同時並行的に取り組む計画である.2023年度は (A), (B), (C), (D) それぞれに取り組んだ.(A) については,MDDと似た圧縮データ構造である ZDD を用いた疑似ブール制約の符号化について研究を行い,発表した.(B) については,適用できる問題は限定されるものの符号化を用いた極小モデル生成方法を考案することができた.得られた成果を発表する準備を現在行っている.(C) については,また最新の制約への対応を実装したソルバーsCOPが国際ソルバー競技会XCSP3で準優勝 (CSP部門)という成績を収めた.(D) についてはシステム生物学および組合せ遷移問題の解法を研究し,国際会議で4件論文発表した.

Current Status of Research Progress
Current Status of Research Progress

1: Research has progressed more than it was originally planned.

Reason

4年の研究計画の初年度に,4つある研究課題のうち4つに着手し,2つについては初期成果の研究発表まで行うことができた.また1つについては国際ソルバー競技会XCSP3で準優勝 (CSP部門)という成績を収めた.このことから,研究は当初の計画以上に進展していると考えている.

Strategy for Future Research Activity

2024年度は,(B) について研究発表の準備を進め,(C) についてもCOPソルバーの開発を本格的に開始する予定である.

Report

(1 results)
  • 2023 Research-status Report
  • Research Products

    (14 results)

All 2024 2023 Other

All Int'l Joint Research (2 results) Journal Article (4 results) (of which Int'l Joint Research: 2 results,  Peer Reviewed: 4 results,  Open Access: 3 results) Presentation (6 results) (of which Invited: 1 results) Remarks (2 results)

  • [Int'l Joint Research] Centrale Nantes/CRIL-CNRS UMR 8188/Artois University(フランス)

    • Related Report
      2023 Research-status Report
  • [Int'l Joint Research] University of Potsdam(ドイツ)

    • Related Report
      2023 Research-status Report
  • [Journal Article] ZDD-based algorithmic framework for solving shortest reconfiguration problems2023

    • Author(s)
      Takehiro Ito, Jun Kawahara, Yu Nakahata, Takehide Soh, Akira Suzuki, Junichi Teruyama and Takahisa Toda
    • Journal Title

      Proceedings of the 20th International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR 2023), Lecture Notes in Computer Science (LNCS)

      Volume: 13884 Pages: 1-17

    • DOI

      10.1007/978-3-031-33271-5_12

    • ISBN
      9783031332708, 9783031332715
    • Related Report
      2023 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] Solving reconfiguration problems of first-order expressible properties of graph vertices with Boolean satisfiability2023

    • Author(s)
      Takahisa Toda, Takehiro Ito, Jun Kawahara, Takehide Soh, Akira Suzuki, Junichi Teruyama
    • Journal Title

      Proc. of 35th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2023)

      Volume: - Pages: 294-302

    • DOI

      10.1109/ictai59109.2023.00050

    • Related Report
      2023 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] Hamiltonian Cycle Reconfiguration with Answer Set Programming2023

    • Author(s)
      Hirate Takahiro、Banbara Mutsunori、Inoue Katsumi、Lu Xiao-Nan、Nabeshima Hidetomo、Schaub Torsten、Soh Takehide、Tamura Naoyuki
    • Journal Title

      Proceedings of the 18th European Conference on Logics in Artificial Intelligence (JELIA 2023)

      Volume: LNAI 14281 Pages: 262-277

    • DOI

      10.1007/978-3-031-43619-2_19

    • ISBN
      9783031436185, 9783031436192
    • Related Report
      2023 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] SAF: SAT-Based Attractor Finder in?Asynchronous Automata Networks2023

    • Author(s)
      Soh Takehide、Magnin Morgan、Le Berre Daniel、Banbara Mutsunori、Tamura Naoyuki
    • Journal Title

      Proceedings of the 21st International Conference on Computational Methods in Systems Biology (CMSB 2023)

      Volume: LNCS 14137 Pages: 175-183

    • DOI

      10.1007/978-3-031-42697-1_12

    • ISBN
      9783031426964, 9783031426971
    • Related Report
      2023 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Presentation] 解集合プログラミングを用いた支配集合遷移2024

    • Author(s)
      加藤聖人, 宋剛秀, 田村直之, 番原睦則
    • Organizer
      第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
    • Related Report
      2023 Research-status Report
  • [Presentation] heulingo: 組合せ最適化のための解集合プログラミングに基づく優先度付き巨大近傍探索の実装2024

    • Author(s)
      杉森唯瑠未, 宋剛秀, 田村直之, 井上克巳, 鍋島英知, 番原睦則
    • Organizer
      第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
    • Related Report
      2023 Research-status Report
  • [Presentation] ZDDを用いた疑似ブール制約のSAT符号化2023

    • Author(s)
      大橋 瞭雅, 宋 剛秀
    • Organizer
      人工知能基本問題研究会
    • Related Report
      2023 Research-status Report
  • [Presentation] 最大独立集合問題のSAT技術を用いた解法に関する研究2023

    • Author(s)
      大森 嶺, 宋 剛秀, 田村 直之
    • Organizer
      2023年度人工知能学会全国大会(第37回)
    • Related Report
      2023 Research-status Report
  • [Presentation] SATソルバーとその応用について2023

    • Author(s)
      宋 剛秀
    • Organizer
      電子情報通信学会ソサエティ大会
    • Related Report
      2023 Research-status Report
    • Invited
  • [Presentation] 解集合プログラミングを用いた支配集合遷移問題の解法に関する考察2023

    • Author(s)
      加藤聖人, 宋剛秀, 田村直之, 番原睦則
    • Organizer
      2023年度人工知能学会全国大会 (第37回)
    • Related Report
      2023 Research-status Report
  • [Remarks] 研究業績リスト (宋 剛秀)

    • URL

      https://tsoh.org/publication/

    • Related Report
      2023 Research-status Report
  • [Remarks] Fun-sCOP

    • URL

      https://tsoh.org/fun-scop/

    • Related Report
      2023 Research-status Report

URL: 

Published: 2023-04-13   Modified: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi