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

SAT符号化を用いた制約解集合プログラミングに関する研究開発

研究課題

研究課題/領域番号 15K00099
研究種目

基盤研究(C)

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

研究代表者

番原 睦則  神戸大学, 情報基盤センター, 准教授 (80290774)

研究分担者 田村 直之  神戸大学, 情報基盤センター, 教授 (60207248)
宋 剛秀  神戸大学, 情報基盤センター, 助教 (00625121)
連携研究者 井上 克巳  国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321)
研究期間 (年度) 2015-04-01 – 2018-03-31
研究課題ステータス 完了 (2017年度)
配分額 *注記
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2017年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2016年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2015年度: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円)
キーワード解集合プログラミング / 制約プログラミング / SAT技術 / SAT
研究成果の概要

本研究では,解集合プログラミング(ASP; Answer Set Programming)と制約プログラミング(CP; Constraint Programming)を融合した制約解集合プログラミング(以下,制約ASP)に関する研究開発を行った.制約ASPは,制約充足問題(CPの言語)を取り扱えるように言語拡張されており,整数の有限領域上の算術制約などを直接表現できる.事前処理型と遅延処理型の2種類の制約ASPソルバーの設計・実装・評価を行い,その有効性を示した.

報告書

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

    (53件)

すべて 2018 2017 2016 2015 その他

すべて 国際共同研究 (7件) 雑誌論文 (18件) (うち国際共著 11件、 査読あり 17件、 オープンアクセス 8件、 謝辞記載あり 2件) 学会発表 (28件) (うち招待講演 3件)

  • [国際共同研究] ポツダム大学(ドイツ)

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

    • 関連する報告書
      2017 実績報告書
  • [国際共同研究] ポツダム大学(ドイツ)

    • 関連する報告書
      2016 実施状況報告書
  • [国際共同研究] University of Potsdam(ドイツ)

    • 関連する報告書
      2015 実施状況報告書
  • [国際共同研究] Aalto University(フィンランド)

    • 関連する報告書
      2015 実施状況報告書
  • [国際共同研究] University of Ferrara(イタリア)

    • 関連する報告書
      2015 実施状況報告書
  • [国際共同研究] INRIA Rennes(フランス)

    • 関連する報告書
      2015 実施状況報告書
  • [雑誌論文] 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 実績報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Clingcon: The Next Generation2017

    • 著者名/発表者名
      Mutsunori Banbara, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub
    • 雑誌名

      Theory and Practice of Logic Programming

      巻: 17(4) 号: 4 ページ: 408-461

    • DOI

      10.1017/s1471068417000138

    • 関連する報告書
      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 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] 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 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] 解集合プログラミングによるカリキュラムベース・コース時間割編成2017

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

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

      巻: - ページ: 73-88

    • 関連する報告書
      2017 実績報告書
    • 国際共著
  • [雑誌論文] SAT型制約プログラミングシステムと周辺技術2017

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

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

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

    • DOI

      10.11309/jssst.34.1_67

    • NAID

      130006855237

    • ISSN
      0289-6540
    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Modeling Delayed Dynamics in Biological Regulatory Networks from Time Series Data2017

    • 著者名/発表者名
      Emna Ben Abdallah, Tony Ribeiro, Morgan Magnin, Olivier H. Roux, Katsumi Inoue
    • 雑誌名

      Algorithms

      巻: 10(1) 号: 1 ページ: 8-8

    • DOI

      10.3390/a10010008

    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Analyzing resilience properties in oscillatory biological systems using parametric model checking2016

    • 著者名/発表者名
      Alexander Andreychenko, Morgan Magnin, Katsumi Inoue
    • 雑誌名

      BioSystems

      巻: 149 ページ: 50-58

    • DOI

      10.1016/j.biosystems.2016.09.002

    • 関連する報告書
      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) ページ: 704-709

    • 関連する報告書
      2016 実施状況報告書
    • 査読あり
  • [雑誌論文] SATとパズル2016

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

      情報処理

      巻: 57(8) ページ: 710-715

    • 関連する報告書
      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)

      巻: - ページ: 13-32

    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著 / 謝辞記載あり
  • [雑誌論文] \sum_x-Optimal Solutions in Highly Symmetric Multi-Objective Timetabling Problems2016

    • 著者名/発表者名
      Maxime Clement, Tenda Okimoto, Katsumi Inoue, and Mutsunori Banbara
    • 雑誌名

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

      巻: - ページ: 63-79

    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著 / 謝辞記載あり
  • [雑誌論文] Inference of Delayed Biological Regulatory Networks from Time Series Data2016

    • 著者名/発表者名
      Emna Ben Abdallah, Tony Ribeiro, Morgan Magnin, Olivier F. Roux, Katsumi Inoue
    • 雑誌名

      Proc. 14th Int'l Conf. on Computational Methods in Systems Biology (CMSB 2016), Lecture Notes in Bioinformatics

      巻: 9859 ページ: 30-48

    • DOI

      10.1007/978-3-319-45177-0_3

    • ISBN
      9783319451763, 9783319451770
    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / 国際共著
  • [雑誌論文] A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings2015

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

      Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2015, SAT and CSP track)

      巻: - ページ: 421-428

    • DOI

      10.1109/ictai.2015.70

    • NAID

      40020657481

    • 関連する報告書
      2015 実施状況報告書
    • 査読あり
  • [雑誌論文] aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming2015

    • 著者名/発表者名
      Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, Torsten Schaub, Takehide Soh, Naoyuki Tamura, and Matthias Weise
    • 雑誌名

      Proceedings of the 13th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2015)

      巻: LNAI9345 ページ: 112-126

    • DOI

      10.1007/978-3-319-23264-5_10

    • ISBN
      9783319232638, 9783319232645
    • 関連する報告書
      2015 実施状況報告書
    • 査読あり / 国際共著
  • [学会発表] SAT ソルバーの進歩2017

    • 著者名/発表者名
      番原睦則
    • 学会等名
      2017年電子情報通信学会総合大会
    • 発表場所
      名城大学 (愛知県・名古屋市)
    • 年月日
      2017-03-22
    • 関連する報告書
      2016 実施状況報告書
    • 招待講演
  • [学会発表] ブール基数制約を経由した擬似ブール制約の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ソルバーの最新動向と利用技術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 実施状況報告書
  • [学会発表] 解集合プログラミングによるカリキュラムベース・コース時間割編成2017

    • 著者名/発表者名
      番原睦則
    • 学会等名
      第29回RAMPシンポジウム
    • 関連する報告書
      2017 実績報告書
    • 招待講演
  • [学会発表] SAT から解集合プログラミングへ2017

    • 著者名/発表者名
      番原睦則
    • 学会等名
      人工知能学会全国大会(第31回) オーガナイズドセッション「OS-2 SAT技術の理論,実装,応用」
    • 関連する報告書
      2017 実績報告書
    • 招待講演
  • [学会発表] ブール基数制約を経由した擬似ブール制約のSAT符号化手法2017

    • 著者名/発表者名
      南雄之, 宋剛秀, 番原睦則, 田村直之
    • 学会等名
      日本ソフトウェア科学会第34回大会
    • 関連する報告書
      2017 実績報告書
  • [学会発表] 解集合プログラミングを用いた3次元ナンバーリンクソルバー2017

    • 著者名/発表者名
      坡山直樹, 飯野有軌, 番原睦則, 田村直之
    • 学会等名
      DAシンポジウム2017
    • 関連する報告書
      2017 実績報告書
  • [学会発表] SAT技術を用いたペトリネットのデッドロック検出手法の提案2017

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

    • 著者名/発表者名
      坡山直樹, 番原睦則, 宋剛秀, 田村直之
    • 学会等名
      人工知能学会全国大会(第31回)
    • 関連する報告書
      2017 実績報告書
  • [学会発表] 解集合プログラミングを用いたナンバーリンクの解法に関する一考察2016

    • 著者名/発表者名
      坡山直樹, 川原征大, 迫龍哉, 番原睦則
    • 学会等名
      DAシンポジウム2016
    • 発表場所
      ゆのくに天祥 (石川県・加賀市)
    • 年月日
      2016-09-14
    • 関連する報告書
      2016 実施状況報告書
  • [学会発表] 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 実施状況報告書
  • [学会発表] クラウド上のソフトウェア要素最適配置問題の解法2016

    • 著者名/発表者名
      田村直之, 井上克巳, 鍋島英知, 番原睦則, 宋剛秀
    • 学会等名
      人工知能基本問題研究会(第100回)
    • 発表場所
      熊本市民会館 (熊本県熊本市中央区桜町)
    • 年月日
      2016-03-27
    • 関連する報告書
      2015 実施状況報告書
  • [学会発表] 解集合プログラミングを用いた制約組合せテストケース生成2016

    • 著者名/発表者名
      兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳, 沖本天太
    • 学会等名
      第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016)
    • 発表場所
      ダイヤモンド瀬戸内マリンホテル(岡山県玉野市渋川)
    • 年月日
      2016-03-07
    • 関連する報告書
      2015 実施状況報告書
  • [学会発表] インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー2016

    • 著者名/発表者名
      迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知
    • 学会等名
      第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016)
    • 発表場所
      ダイヤモンド瀬戸内マリンホテル (岡山県玉野市渋川)
    • 年月日
      2016-03-07
    • 関連する報告書
      2015 実施状況報告書
  • [学会発表] SATソルバーを用いた制約プログラミングシステムとその応用2016

    • 著者名/発表者名
      宋剛秀
    • 学会等名
      第57回プログラミング・シンポジウム
    • 発表場所
      ラフォーレ倶楽部伊東温泉湯の庭 (静岡県伊東市猪戸)
    • 年月日
      2016-01-08
    • 関連する報告書
      2015 実施状況報告書
  • [学会発表] \Sigma-Optimal Solutions in Multi-Objective Timetabling2015

    • 著者名/発表者名
      Maxime Clement, Tenda Okimoto, Katsumi Inoue, and Mutsunori Banbara
    • 学会等名
      合同エージェントワークショップ&シンポジウム2015論文集 (JAWS 2015)
    • 発表場所
      山中温泉河鹿荘ロイヤルホテル (石川県加賀市山中温泉河鹿町)
    • 年月日
      2015-09-30
    • 関連する報告書
      2015 実施状況報告書
  • [学会発表] SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価2015

    • 著者名/発表者名
      川原征大, 宋剛秀, 番原睦則, 田村直之
    • 学会等名
      日本ソフトウェア科学会第32回大会
    • 発表場所
      早稲田大学西早稲田キャンパス(東京都新宿区大久保)
    • 年月日
      2015-09-09
    • 関連する報告書
      2015 実施状況報告書
  • [学会発表] iSugar : インクリメンタルSAT解法が利用可能なSAT型制約ソルバー2015

    • 著者名/発表者名
      迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
    • 学会等名
      日本ソフトウェア科学会第32回大会
    • 発表場所
      早稲田大学西早稲田キャンパス(東京都新宿区大久保)
    • 年月日
      2015-09-09
    • 関連する報告書
      2015 実施状況報告書
  • [学会発表] 順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化2015

    • 著者名/発表者名
      宋剛秀, 番原睦則, 田村直之
    • 学会等名
      日本ソフトウェア科学会第32回大会
    • 発表場所
      早稲田大学西早稲田キャンパス(東京都新宿区大久保)
    • 年月日
      2015-09-09
    • 関連する報告書
      2015 実施状況報告書
  • [学会発表] SAT型制約ソルバーによるナンバーリンクの求解と解の最適化2015

    • 著者名/発表者名
      迫龍哉, 川原征大, 田村直之, 番原睦則, 宋剛秀, 鍋島英知
    • 学会等名
      情報処理学会システムとLSIの設計技術研究会
    • 発表場所
      山代温泉ゆのくに天祥 (石川県加賀市山代温泉19-49-1)
    • 年月日
      2015-08-26
    • 関連する報告書
      2015 実施状況報告書
  • [学会発表] 組合せテストケース生成問題に対する制約解集合プログラミングの適用2015

    • 著者名/発表者名
      兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳
    • 学会等名
      2015年度人工知能学会全国大会(第29回)
    • 発表場所
      公立はこだて未来大学 (北海道函館市亀田中野町)
    • 年月日
      2015-05-30
    • 関連する報告書
      2015 実施状況報告書

URL: 

公開日: 2015-04-16   更新日: 2019-03-29  

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

Powered by NII kakenhi