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

High Performance SAT-based Constraint Programming System using Hybrid Encoding

Research Project

Project/Area Number 16K16036
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeMulti-year Fund
Research Field Software
Research InstitutionKobe University

Principal Investigator

Soh Takehide  神戸大学, 情報基盤センター, 助教 (00625121)

Project Period (FY) 2016-04-01 – 2019-03-31
Project Status Completed (Fiscal Year 2018)
Budget Amount *help
¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2018: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2017: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2016: ¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
KeywordsSATソルバー / SAT符号化 / 順序符号化 / 対数符号化 / ハイブリッド符号化 / 制約充足問題 / 制約プログラミング / 情報システム
Outline of Final Research Achievements

Constraint Satisfaction Problem (CSP) is a problem of finding an assignment that satisfies all the given constraints. CSP has various applications in both academia and industry and it is recognized as an important problem in the research area of Artificial Intelligence. In this research, we study a hybrid encoding method to realize a high performance CSP solving system using SAT solvers (SAT-based CP System). As a result, we succeeded in winning an international competition and solving problems that cannot be solved by existing systems.

Academic Significance and Societal Importance of the Research Achievements

本研究成果の意義は,SAT符号化の新しい方向性を開拓した点,既存のCPシステムでは求解困難な問題に対して,より高性能な推論基盤の候補を提供した点である.また重要な応用の1つとして,システム生物学やグラフ上の問題にも適用可能な多目的最適化問題への応用を示したことも挙げられる.CPシステムは様々な分野に応用される実用性が高いシステムであり,研究成果の産業分野への応用も期待できると考えられる.

Report

(4 results)
  • 2018 Annual Research Report   Final Research Report ( PDF )
  • 2017 Research-status Report
  • 2016 Research-status Report
  • Research Products

    (41 results)

All 2019 2018 2017 2016 Other

All Int'l Joint Research (3 results) Journal Article (14 results) (of which Int'l Joint Research: 6 results,  Peer Reviewed: 12 results,  Open Access: 9 results,  Acknowledgement Compliant: 1 results) Presentation (18 results) (of which Int'l Joint Research: 1 results) Remarks (5 results) Funded Workshop (1 results)

  • [Int'l Joint Research] CRIL-CNRS, Artois University(フランス)

    • Related Report
      2018 Annual Research Report
  • [Int'l Joint Research] アルトワ大学(フランス)

    • Related Report
      2017 Research-status Report
  • [Int'l Joint Research] アルトワ大学, CRIL-CNRS UMR 8188(フランス)

    • Related Report
      2016 Research-status Report
  • [Journal Article] A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints2018

    • Author(s)
      南雄之, 宋剛秀, 番原睦則, 田村直之
    • Journal Title

      Computer Software

      Volume: 35 Issue: 3 Pages: 3_65-3_78

    • DOI

      10.11309/jssst.35.3_65

    • NAID

      130007487601

    • ISSN
      0289-6540
    • Year and Date
      2018-07-25
    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] SATソルバーの最新動向と利用技術2018

    • Author(s)
      宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
    • Journal Title

      コンピュータソフトウェア

      Volume: 35(4) Pages: 72-92

    • NAID

      130007552525

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] SAT技術を用いたペトリネットのデッドロック検出手法の提案2018

    • Author(s)
      寸田 智也, 宋 剛秀, 番原 睦則, 田村 直之, 井上 克巳
    • Journal Title

      情報処理学会論文誌

      Volume: 59(9) Pages: 1749-1760

    • NAID

      130007425532

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed
  • [Journal Article] sCOP: SAT-based Constraint Programming System2018

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

      Proceedings of XCSP3 Competition 2018

      Volume: なし Pages: 93-94

    • Related Report
      2018 Annual Research Report
    • Open Access / Int'l Joint Research
  • [Journal Article] teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming2018

    • Author(s)
      Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
    • Journal Title

      Annals of Operations Research

      Volume: - Issue: 1 Pages: 3-37

    • DOI

      10.1007/s10479-018-2757-7

    • Related Report
      2017 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Proposal and Evaluation of Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings2017

    • Author(s)
      Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
    • Journal Title

      International Journal on Artificial Intelligence Tools

      Volume: 26(1) Issue: 01 Pages: 1760005-1760005

    • DOI

      10.1142/s0218213017600053

    • Related Report
      2017 Research-status Report 2016 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] Solving Multiobjective Discrete Optimization Problems with Propositional Minimal Model Generation2017

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

      Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP 2017)

      Volume: 10416 Pages: 596-614

    • DOI

      10.1007/978-3-319-66158-2_38

    • ISBN
      9783319661575, 9783319661582
    • Related Report
      2017 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] 解集合プログラミングによるカリキュラムベース・コース時間割編成2017

    • Author(s)
      番原睦則, 井上克巳, ベンジャミン カウフマン, トルステン シャウブ, 宋剛秀, 田村直之, フィリップ ワンコ
    • Journal Title

      第29回RAMPシンポジウム論文集

      Volume: - Pages: 73-88

    • Related Report
      2017 Research-status Report
    • Int'l Joint Research
  • [Journal Article] catnap: Generating Test Suites of Constrained Combinatorial Testing with Answer Set Programming2017

    • Author(s)
      Mutsunori Banbara, Katsumi Inoue, Hiromasa Kaneyuki, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura
    • Journal Title

      Proceedings of the 14th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2017)

      Volume: 10377 Pages: 265-278

    • DOI

      10.1007/978-3-319-61660-5_24

    • ISBN
      9783319616599, 9783319616605
    • Related Report
      2017 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] SAT-based Constraint Programming Systems and Related Technologies2017

    • Author(s)
      宋剛秀, 番原睦則, 田村直之
    • Journal Title

      Computer Software

      Volume: 34 Issue: 1 Pages: 1_67-1_80

    • DOI

      10.11309/jssst.34.1_67

    • NAID

      130006855237

    • ISSN
      0289-6540
    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] An Incremental SAT Solving Library and its Applications2016

    • Author(s)
      迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
    • Journal Title

      Computer Software

      Volume: 33 Issue: 4 Pages: 4_16-4_29

    • DOI

      10.11309/jssst.33.4_16

    • NAID

      130005290581

    • ISSN
      0289-6540
    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] SATとパズル2016

    • Author(s)
      田村直之, 宋剛秀, 番原睦則
    • Journal Title

      情報処理

      Volume: 57(8)

    • Related Report
      2016 Research-status Report
    • Peer Reviewed
  • [Journal Article] Implementing Efficient All Solutions SAT Solvers2016

    • Author(s)
      Takahisa Toda, Takehide Soh
    • Journal Title

      Journal of Experimental Algorithmics

      Volume: 21(1) Pages: 1-44

    • DOI

      10.1145/2975585

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming2016

    • Author(s)
      Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Torsten Schaub, Takehide Soh, Naoyuki Tamura, and Philipp Wanko
    • Journal Title

      Proceedings of the 11th International Conference on the Practice and Theory of Automated Timetabling (PATAT 2016)

      Volume: なし

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Presentation] alldifferent制約のブール基数制約への符号化手法の提案とクイーングラフ彩色問題への応用2019

    • Author(s)
      大野 周亮, 番原 睦則, 宋 剛秀, 田村 直之
    • Organizer
      人工知能学会 第109回人工知能基本問題研究会
    • Related Report
      2018 Annual Research Report
  • [Presentation] 正規制約のSAT符号化とその性能評価2018

    • Author(s)
      生田 哲也, 田村 直之, 番原 睦則, 宋 剛秀
    • Organizer
      日本ソフトウェア科学会 第35回大会
    • Related Report
      2018 Annual Research Report
  • [Presentation] SATソルバーを用いた様相命題論理S4の充足可能性判定2018

    • Author(s)
      飯野 有軌, 田村 直之, 番原 睦則, 宋 剛秀
    • Organizer
      日本ソフトウェア科学会 第35回大会
    • Related Report
      2018 Annual Research Report
  • [Presentation] teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming2018

    • Author(s)
      Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
    • Organizer
      The 28th International Conference on Automated Planning and Scheduling (ICAPS 2018)
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] ブール基数制約を経由した擬似ブール制約のSAT符号化法2017

    • Author(s)
      南雄之, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      人工知能基本問題研究会(第103回)
    • Place of Presentation
      湯布院公民館 (大分県・由布市)
    • Year and Date
      2017-03-13
    • Related Report
      2016 Research-status Report
  • [Presentation] 解集合プログラミングを用いた多層ナンバーリンクの解法2017

    • Author(s)
      坡山直樹, 川原征大, 迫龍哉, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)
    • Place of Presentation
      華やぎの章 慶山 (山梨県・笛吹市)
    • Year and Date
      2017-03-08
    • Related Report
      2016 Research-status Report
  • [Presentation] SugarTracer: SAT型制約ソルバーSugarのトレースツール2017

    • Author(s)
      吉玉元和, 寸田智也, 南雄之, 宋剛秀, 番原睦則, 田村 直之
    • Organizer
      第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)
    • Place of Presentation
      華やぎの章 慶山 (山梨県・笛吹市)
    • Year and Date
      2017-03-08
    • Related Report
      2016 Research-status Report
  • [Presentation] SATソルバーの最新動向と利用技術 (PPL2017発表賞(一般の部)受賞)2017

    • Author(s)
      宋剛秀, 田村直之
    • Organizer
      第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)
    • Place of Presentation
      華やぎの章 慶山 (山梨県・笛吹市)
    • Year and Date
      2017-03-08
    • Related Report
      2016 Research-status Report
  • [Presentation] SATソルバーの使い方 ―問題をSATに符号化する方法―2017

    • Author(s)
      田村直之, 宋剛秀, 番原睦則
    • Organizer
      第58回プログラミング・シンポジウム
    • Place of Presentation
      ラフォーレ伊東 (静岡県・伊東市)
    • Year and Date
      2017-01-06
    • Related Report
      2016 Research-status Report
  • [Presentation] Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー2017

    • Author(s)
      宋剛秀,番原睦則,田村直之
    • Organizer
      第58回プログラミング・シンポジウム
    • Place of Presentation
      ラフォーレ伊東 (静岡県・伊東市)
    • Year and Date
      2017-01-06
    • Related Report
      2016 Research-status Report
  • [Presentation] ブール基数制約を経由した擬似ブール制約のSAT符号化手法2017

    • Author(s)
      南雄之, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      日本ソフトウェア科学会第34回大会
    • Related Report
      2017 Research-status Report
  • [Presentation] SAT型制約ソルバーを用いた3次元ナンバーリンクの解法2017

    • Author(s)
      寸田智也, 南雄之, 宋剛秀, 田村直之
    • Organizer
      DAシンポジウム2017
    • Related Report
      2017 Research-status Report
  • [Presentation] SAT技術を用いたペトリネットのデッドロック検出手法の提案2017

    • Author(s)
      寸田智也, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      人工知能学会全国大会(第31回)
    • Related Report
      2017 Research-status Report
  • [Presentation] 制約充足問題のASP符号化に関する一考察2017

    • Author(s)
      坡山直樹, 番原睦則, 宋剛秀, 田村直之
    • Organizer
      人工知能学会全国大会(第31回)
    • Related Report
      2017 Research-status Report
  • [Presentation] SAT型制約ソルバーを用いた多層ナンバーリンクの解法2016

    • Author(s)
      寸田智也, 南雄之, 吉玉元和, 宋剛秀
    • Organizer
      DAシンポジウム2016
    • Place of Presentation
      ゆのくに天祥 (石川県・加賀市)
    • Year and Date
      2016-09-14
    • Related Report
      2016 Research-status Report
  • [Presentation] SAT技術を用いた正規ペトリネットのデッドロック検出手法の提案2016

    • Author(s)
      寸田智也, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      日本ソフトウェア科学会第33回大会
    • Place of Presentation
      東北大学 (宮城県・仙台市)
    • Year and Date
      2016-09-06
    • Related Report
      2016 Research-status Report
  • [Presentation] SATソルバーを用いた部分グラフ探索のための制約モデル2016

    • Author(s)
      川原征大, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      2016年度 人工知能学会全国大会
    • Place of Presentation
      北九州国際会議場 (福岡県・北九州市)
    • Year and Date
      2016-06-06
    • Related Report
      2016 Research-status Report
  • [Presentation] SAT型制約ソルバーによるナンバーリンクの解法とその評価 (全国大会優秀賞受賞)2016

    • Author(s)
      迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知
    • Organizer
      2016年度 人工知能学会全国大会
    • Place of Presentation
      北九州国際会議場 (福岡県・北九州市)
    • Year and Date
      2016-06-06
    • Related Report
      2016 Research-status Report
  • [Remarks] sCOP: a SAT-based CP System

    • URL

      https://tsoh.org/sCOP/

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

    • URL

      http://kix.istc.kobe-u.ac.jp/~soh/jp/

    • Related Report
      2017 Research-status Report
  • [Remarks] 宋剛秀の「経歴・実績」ページ

    • URL

      http://kix.istc.kobe-u.ac.jp/~soh/jp/

    • Related Report
      2016 Research-status Report
  • [Remarks] 宋剛秀の「業績」ページ

    • URL

      http://kix.istc.kobe-u.ac.jp/~soh/jp/publications.html

    • Related Report
      2016 Research-status Report
  • [Remarks] Diet-Sugar: SATソルバーを用いたCSPソルバー

    • URL

      http://kix.istc.kobe-u.ac.jp/~soh/dsugar/

    • Related Report
      2016 Research-status Report
  • [Funded Workshop] CRIL-Kobe-Louvain 共同ワークショップ2017

    • Related Report
      2017 Research-status Report

URL: 

Published: 2016-04-21   Modified: 2020-03-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi