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

Acceleration of SAT-based CSP Solvers using MDD

Research Project

Project/Area Number 20K11748
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

Soh Takehide  神戸大学, DX・情報統括本部, 准教授 (00625121)

Project Period (FY) 2020-04-01 – 2023-03-31
Project Status Completed (Fiscal Year 2022)
Budget Amount *help
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2022: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2021: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2020: ¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
KeywordsSATソルバー / SAT符号化 / MDD / 制約充足問題 / 制約プログラミング / SAT (充足可能性判定問題) / CSP (制約充足問題)
Outline of Research at the Start

近年,SAT問題を解くプログラムであるSATソルバーの飛躍的な進歩にともない,制約充足問題 (CSP) をSAT問題に符号化(SAT符号化)して解くSAT型CSPソルバーが成功している.

本研究の目的は,SAT型CSPソルバーの高速化であり,そのためにMDD (Multi-valued Decision Diagram) を用いたCSPの正規化と,MDDが表す制約 (MDD制約) のSAT符号化を研究開発する.

本研究の意義は,SAT型CSPソルバーの新しい一方式を開拓できる点,既存のCSPソルバーでは求解困難な問題に対して,より高性能な推論基盤を提供できる点である.

Outline of Final Research Achievements

Constraint Satisfaction Problem (CSP) is a problem of finding assignments that satisfy given constraints. CSP has various applications across academia and industry, and it is an important research topic in fields such as artificial intelligence. In this study, we conducted research and development on methods using the MDD representation of constraints and SAT encoding to realize a high-performance CSP solving system using a SAT solver (SAT-based CSP solver). As a result, we achieved success in terms of winning in international competitions and speeding up the system. Additionally, we applied SAT-based solving methods to compute the steady state (attractor) of automata networks, which are mathematical models of gene regulatory networks occurring within cells in systems biology. Furthermore, we proposed a SAT-based solving method for the Hamiltonian cycle problem.

Academic Significance and Societal Importance of the Research Achievements

本研究成果の意義は,SAT符号化の新しい方向性を開拓した点,既存のCSPソルバーでは求解困難な問題に対して.より高性能な推論基盤の候補を提供した点である.またシステム生物学における定常状態の解析への応用を示したことも貢献として挙げられる.CSPソルバーは様々な分野に応用される実用性が高いシステムであり,研究成果の産業分野への応用も期待できると考えられる.

Report

(4 results)
  • 2022 Annual Research Report   Final Research Report ( PDF )
  • 2021 Research-status Report
  • 2020 Research-status Report
  • Research Products

    (15 results)

All 2023 2022 2021 2020 Other

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

  • [Int'l Joint Research] CNRS (CRIL)/CNRS (LS2N)(フランス)

    • Related Report
      2022 Annual Research Report
  • [Journal Article] SAT-based Method for Finding Attractors in Asynchronous Multi-valued Networks2023

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

      Proceedings of the 14th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS 2023)

      Volume: - Pages: 163-174

    • DOI

      10.5220/0011675100003414

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Fun-sCOP. XCSP3 Competition 20222022

    • Author(s)
      Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura
    • Journal Title

      In Proceedings of the XCSP3 Competition 2022

      Volume: -

    • Related Report
      2022 Annual Research Report
    • Open Access / Int'l Joint Research
  • [Journal Article] Satisfiability Testing of Propositional Modal Logic K with Answer Set Programming2020

    • Author(s)
      飯野有軌, 田村直之, 宋剛秀, 番原睦則, 井上克巳
    • Journal Title

      Proceedings of the Annual Conference of JSAI

      Volume: JSAI2020 Issue: 0 Pages: 2N5OS17b05-2N5OS17b05

    • DOI

      10.11517/pjsai.JSAI2020.0_2N5OS17b05

    • NAID

      130007856950

    • Related Report
      2020 Research-status Report
    • Open Access
  • [Presentation] 解集合プログラミングを用いたハミルトン閉路遷移問題の解法.2023

    • Author(s)
      平手貴大, 番原睦則, 井上克巳, 盧暁南, 鍋島英知, 宋剛秀, 田村直之.
    • Organizer
      第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
    • Related Report
      2022 Annual Research Report
  • [Presentation] チャネリング制約を用いた alldifferent 制約の SAT 符号化2022

    • Author(s)
      小菅脩司, 宋剛秀, 田村直之, 番原睦則
    • Organizer
      情報処理学会 第84回全国大会
    • Related Report
      2021 Research-status Report
  • [Presentation] 解集合プログラミングを用いた優先度付き巨大近傍探索の実装と評価2022

    • Author(s)
      桑原和也, 宋剛秀, 田村直之, 番原睦則
    • Organizer
      情報処理学会 第84回全国大会
    • Related Report
      2021 Research-status Report
  • [Presentation] Towards CEGAR-based Parallel SAT Solving2021

    • Author(s)
      Takehide Soh, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura and Katsumi Inoue
    • Organizer
      The Pragmatics of SAT Workshop 2021
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] ライフゲームを逆向きに動かす2021

    • Author(s)
      足立啓一, 宋剛秀, 田村直之
    • Organizer
      日本ソフトウェア科学会第38回大会
    • Related Report
      2021 Research-status Report
  • [Presentation] CDCL型SATソルバーの内部動作可視化ツール2021

    • Author(s)
      堀岡真未, 宋剛秀, 田村直之
    • Organizer
      日本ソフトウェア科学会第38回大会
    • Related Report
      2021 Research-status Report
  • [Presentation] SATソルバーを用いた一層平面配置配線問題の解法に関する考察2020

    • Author(s)
      三嶋哲平, 宋剛秀, 田村直之
    • Organizer
      日本ソフトウェア科学会第37回大会
    • Related Report
      2020 Research-status Report
  • [Remarks] XCSP Competitions

    • URL

      http://xcsp.org/competitions/

    • Related Report
      2022 Annual Research Report
  • [Remarks] Supplemental Material for Bioinformatics 2023

    • URL

      https://doi.org/10.5281/zenodo.7460387

    • Related Report
      2022 Annual Research Report
  • [Remarks] 宋 剛秀 (業績,ソフトウェアへのリンク)

    • URL

      https://tsoh.org/

    • Related Report
      2021 Research-status Report 2020 Research-status Report
  • [Remarks] sCOP: a SAT-based CP System

    • URL

      https://tsoh.org/sCOP/

    • Related Report
      2021 Research-status Report 2020 Research-status Report

URL: 

Published: 2020-04-28   Modified: 2024-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi