• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

ハイブリッド符号化を用いた高性能なSAT型制約プログラミングシステム

研究課題

研究課題/領域番号 16K16036
研究種目

若手研究(B)

配分区分基金
研究分野 ソフトウェア
研究機関神戸大学

研究代表者

宋 剛秀  神戸大学, 情報基盤センター, 助教 (00625121)

研究期間 (年度) 2016-04-01 – 2019-03-31
研究課題ステータス 完了 (2018年度)
配分額 *注記
3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2018年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2017年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2016年度: 2,600千円 (直接経費: 2,000千円、間接経費: 600千円)
キーワードSATソルバー / SAT符号化 / 順序符号化 / 対数符号化 / ハイブリッド符号化 / 制約充足問題 / 制約プログラミング / 情報システム
研究成果の概要

制約充足問題 (CSP) は,与えられた制約を満たす解を探索する問題である.CSP には産学問わず様々な応用があり,人工知能分野などにおける重要な研究課題となっている.本研究では, SATソルバーを用いた高性能な CSP を解くシステム (SAT型CPシステム) を実現するために,ハイブリッド符号化を用いた方法を研究開発した.結果として,国際競技会における優勝や, 従来システムでは解けない問題を解くことに成功した.

研究成果の学術的意義や社会的意義

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

報告書

(4件)
  • 2018 実績報告書   研究成果報告書 ( PDF )
  • 2017 実施状況報告書
  • 2016 実施状況報告書

研究成果

(41件)

すべて 2019 2018 2017 2016 その他

すべて 国際共同研究 (3件) 雑誌論文 (14件) (うち国際共著 6件、 査読あり 12件、 オープンアクセス 9件、 謝辞記載あり 1件) 学会発表 (18件) (うち国際学会 1件) 備考 (5件) 学会・シンポジウム開催 (1件)

  • [国際共同研究] CRIL-CNRS, Artois University(フランス)

    • 関連する報告書
      2018 実績報告書
  • [国際共同研究] アルトワ大学(フランス)

    • 関連する報告書
      2017 実施状況報告書
  • [国際共同研究] アルトワ大学, CRIL-CNRS UMR 8188(フランス)

    • 関連する報告書
      2016 実施状況報告書
  • [雑誌論文] ブール基数制約を経由した擬似ブール制約のSAT符号化手法2018

    • 著者名/発表者名
      南雄之, 宋剛秀, 番原睦則, 田村直之
    • 雑誌名

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

      巻: 35 号: 3 ページ: 3_65-3_78

    • DOI

      10.11309/jssst.35.3_65

    • NAID

      130007487601

    • ISSN
      0289-6540
    • 年月日
      2018-07-25
    • 関連する報告書
      2018 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] SATソルバーの最新動向と利用技術2018

    • 著者名/発表者名
      宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
    • 雑誌名

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

      巻: 35(4) ページ: 72-92

    • NAID

      130007552525

    • 関連する報告書
      2018 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] SAT技術を用いたペトリネットのデッドロック検出手法の提案2018

    • 著者名/発表者名
      寸田 智也, 宋 剛秀, 番原 睦則, 田村 直之, 井上 克巳
    • 雑誌名

      情報処理学会論文誌

      巻: 59(9) ページ: 1749-1760

    • NAID

      130007425532

    • 関連する報告書
      2018 実績報告書
    • 査読あり
  • [雑誌論文] sCOP: SAT-based Constraint Programming System2018

    • 著者名/発表者名
      Takehide Soh, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
    • 雑誌名

      Proceedings of XCSP3 Competition 2018

      巻: なし ページ: 93-94

    • 関連する報告書
      2018 実績報告書
    • オープンアクセス / 国際共著
  • [雑誌論文] teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming2018

    • 著者名/発表者名
      Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
    • 雑誌名

      Annals of Operations Research

      巻: - 号: 1 ページ: 3-37

    • DOI

      10.1007/s10479-018-2757-7

    • 関連する報告書
      2017 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Proposal and Evaluation of Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings2017

    • 著者名/発表者名
      Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
    • 雑誌名

      International Journal on Artificial Intelligence Tools

      巻: 26(1) 号: 01 ページ: 1760005-1760005

    • DOI

      10.1142/s0218213017600053

    • 関連する報告書
      2017 実施状況報告書 2016 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Solving Multiobjective Discrete Optimization Problems with Propositional Minimal Model Generation2017

    • 著者名/発表者名
      Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Daniel Le Berre
    • 雑誌名

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

      巻: 10416 ページ: 596-614

    • DOI

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

    • ISBN
      9783319661575, 9783319661582
    • 関連する報告書
      2017 実施状況報告書
    • 査読あり / 国際共著
  • [雑誌論文] 解集合プログラミングによるカリキュラムベース・コース時間割編成2017

    • 著者名/発表者名
      番原睦則, 井上克巳, ベンジャミン カウフマン, トルステン シャウブ, 宋剛秀, 田村直之, フィリップ ワンコ
    • 雑誌名

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

      巻: - ページ: 73-88

    • 関連する報告書
      2017 実施状況報告書
    • 国際共著
  • [雑誌論文] catnap: Generating Test Suites of Constrained Combinatorial Testing with Answer Set Programming2017

    • 著者名/発表者名
      Mutsunori Banbara, Katsumi Inoue, Hiromasa Kaneyuki, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura
    • 雑誌名

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

      巻: 10377 ページ: 265-278

    • DOI

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

    • ISBN
      9783319616599, 9783319616605
    • 関連する報告書
      2017 実施状況報告書
    • 査読あり / 国際共著
  • [雑誌論文] SAT型制約プログラミングシステムと周辺技術2017

    • 著者名/発表者名
      宋剛秀, 番原睦則, 田村直之
    • 雑誌名

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

      巻: 34 号: 1 ページ: 1_67-1_80

    • DOI

      10.11309/jssst.34.1_67

    • NAID

      130006855237

    • ISSN
      0289-6540
    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] インクリメンタルSAT解法ライブラリとその応用2016

    • 著者名/発表者名
      迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
    • 雑誌名

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

      巻: 33 号: 4 ページ: 4_16-4_29

    • DOI

      10.11309/jssst.33.4_16

    • NAID

      130005290581

    • ISSN
      0289-6540
    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] SATとパズル2016

    • 著者名/発表者名
      田村直之, 宋剛秀, 番原睦則
    • 雑誌名

      情報処理

      巻: 57(8)

    • 関連する報告書
      2016 実施状況報告書
    • 査読あり
  • [雑誌論文] Implementing Efficient All Solutions SAT Solvers2016

    • 著者名/発表者名
      Takahisa Toda, Takehide Soh
    • 雑誌名

      Journal of Experimental Algorithmics

      巻: 21(1) ページ: 1-44

    • DOI

      10.1145/2975585

    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming2016

    • 著者名/発表者名
      Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Torsten Schaub, Takehide Soh, Naoyuki Tamura, and Philipp Wanko
    • 雑誌名

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

      巻: なし

    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著 / 謝辞記載あり
  • [学会発表] alldifferent制約のブール基数制約への符号化手法の提案とクイーングラフ彩色問題への応用2019

    • 著者名/発表者名
      大野 周亮, 番原 睦則, 宋 剛秀, 田村 直之
    • 学会等名
      人工知能学会 第109回人工知能基本問題研究会
    • 関連する報告書
      2018 実績報告書
  • [学会発表] 正規制約のSAT符号化とその性能評価2018

    • 著者名/発表者名
      生田 哲也, 田村 直之, 番原 睦則, 宋 剛秀
    • 学会等名
      日本ソフトウェア科学会 第35回大会
    • 関連する報告書
      2018 実績報告書
  • [学会発表] SATソルバーを用いた様相命題論理S4の充足可能性判定2018

    • 著者名/発表者名
      飯野 有軌, 田村 直之, 番原 睦則, 宋 剛秀
    • 学会等名
      日本ソフトウェア科学会 第35回大会
    • 関連する報告書
      2018 実績報告書
  • [学会発表] teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming2018

    • 著者名/発表者名
      Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
    • 学会等名
      The 28th International Conference on Automated Planning and Scheduling (ICAPS 2018)
    • 関連する報告書
      2018 実績報告書
    • 国際学会
  • [学会発表] ブール基数制約を経由した擬似ブール制約のSAT符号化法2017

    • 著者名/発表者名
      南雄之, 宋剛秀, 番原睦則, 田村直之
    • 学会等名
      人工知能基本問題研究会(第103回)
    • 発表場所
      湯布院公民館 (大分県・由布市)
    • 年月日
      2017-03-13
    • 関連する報告書
      2016 実施状況報告書
  • [学会発表] 解集合プログラミングを用いた多層ナンバーリンクの解法2017

    • 著者名/発表者名
      坡山直樹, 川原征大, 迫龍哉, 宋剛秀, 番原睦則, 田村直之
    • 学会等名
      第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)
    • 発表場所
      華やぎの章 慶山 (山梨県・笛吹市)
    • 年月日
      2017-03-08
    • 関連する報告書
      2016 実施状況報告書
  • [学会発表] SugarTracer: SAT型制約ソルバーSugarのトレースツール2017

    • 著者名/発表者名
      吉玉元和, 寸田智也, 南雄之, 宋剛秀, 番原睦則, 田村 直之
    • 学会等名
      第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)
    • 発表場所
      華やぎの章 慶山 (山梨県・笛吹市)
    • 年月日
      2017-03-08
    • 関連する報告書
      2016 実施状況報告書
  • [学会発表] SATソルバーの最新動向と利用技術 (PPL2017発表賞(一般の部)受賞)2017

    • 著者名/発表者名
      宋剛秀, 田村直之
    • 学会等名
      第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)
    • 発表場所
      華やぎの章 慶山 (山梨県・笛吹市)
    • 年月日
      2017-03-08
    • 関連する報告書
      2016 実施状況報告書
  • [学会発表] SATソルバーの使い方 ―問題をSATに符号化する方法―2017

    • 著者名/発表者名
      田村直之, 宋剛秀, 番原睦則
    • 学会等名
      第58回プログラミング・シンポジウム
    • 発表場所
      ラフォーレ伊東 (静岡県・伊東市)
    • 年月日
      2017-01-06
    • 関連する報告書
      2016 実施状況報告書
  • [学会発表] Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー2017

    • 著者名/発表者名
      宋剛秀,番原睦則,田村直之
    • 学会等名
      第58回プログラミング・シンポジウム
    • 発表場所
      ラフォーレ伊東 (静岡県・伊東市)
    • 年月日
      2017-01-06
    • 関連する報告書
      2016 実施状況報告書
  • [学会発表] ブール基数制約を経由した擬似ブール制約のSAT符号化手法2017

    • 著者名/発表者名
      南雄之, 宋剛秀, 番原睦則, 田村直之
    • 学会等名
      日本ソフトウェア科学会第34回大会
    • 関連する報告書
      2017 実施状況報告書
  • [学会発表] SAT型制約ソルバーを用いた3次元ナンバーリンクの解法2017

    • 著者名/発表者名
      寸田智也, 南雄之, 宋剛秀, 田村直之
    • 学会等名
      DAシンポジウム2017
    • 関連する報告書
      2017 実施状況報告書
  • [学会発表] SAT技術を用いたペトリネットのデッドロック検出手法の提案2017

    • 著者名/発表者名
      寸田智也, 宋剛秀, 番原睦則, 田村直之
    • 学会等名
      人工知能学会全国大会(第31回)
    • 関連する報告書
      2017 実施状況報告書
  • [学会発表] 制約充足問題のASP符号化に関する一考察2017

    • 著者名/発表者名
      坡山直樹, 番原睦則, 宋剛秀, 田村直之
    • 学会等名
      人工知能学会全国大会(第31回)
    • 関連する報告書
      2017 実施状況報告書
  • [学会発表] SAT型制約ソルバーを用いた多層ナンバーリンクの解法2016

    • 著者名/発表者名
      寸田智也, 南雄之, 吉玉元和, 宋剛秀
    • 学会等名
      DAシンポジウム2016
    • 発表場所
      ゆのくに天祥 (石川県・加賀市)
    • 年月日
      2016-09-14
    • 関連する報告書
      2016 実施状況報告書
  • [学会発表] SAT技術を用いた正規ペトリネットのデッドロック検出手法の提案2016

    • 著者名/発表者名
      寸田智也, 宋剛秀, 番原睦則, 田村直之
    • 学会等名
      日本ソフトウェア科学会第33回大会
    • 発表場所
      東北大学 (宮城県・仙台市)
    • 年月日
      2016-09-06
    • 関連する報告書
      2016 実施状況報告書
  • [学会発表] SATソルバーを用いた部分グラフ探索のための制約モデル2016

    • 著者名/発表者名
      川原征大, 宋剛秀, 番原睦則, 田村直之
    • 学会等名
      2016年度 人工知能学会全国大会
    • 発表場所
      北九州国際会議場 (福岡県・北九州市)
    • 年月日
      2016-06-06
    • 関連する報告書
      2016 実施状況報告書
  • [学会発表] SAT型制約ソルバーによるナンバーリンクの解法とその評価 (全国大会優秀賞受賞)2016

    • 著者名/発表者名
      迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知
    • 学会等名
      2016年度 人工知能学会全国大会
    • 発表場所
      北九州国際会議場 (福岡県・北九州市)
    • 年月日
      2016-06-06
    • 関連する報告書
      2016 実施状況報告書
  • [備考] sCOP: a SAT-based CP System

    • URL

      https://tsoh.org/sCOP/

    • 関連する報告書
      2018 実績報告書
  • [備考] 宋 剛秀 (業績,ソフトウェアへのリンク)

    • URL

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

    • 関連する報告書
      2017 実施状況報告書
  • [備考] 宋剛秀の「経歴・実績」ページ

    • URL

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

    • 関連する報告書
      2016 実施状況報告書
  • [備考] 宋剛秀の「業績」ページ

    • URL

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

    • 関連する報告書
      2016 実施状況報告書
  • [備考] Diet-Sugar: SATソルバーを用いたCSPソルバー

    • URL

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

    • 関連する報告書
      2016 実施状況報告書
  • [学会・シンポジウム開催] CRIL-Kobe-Louvain 共同ワークショップ2017

    • 関連する報告書
      2017 実施状況報告書

URL: 

公開日: 2016-04-21   更新日: 2020-03-30  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi