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

2016 年度 実施状況報告書

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

研究課題

研究課題/領域番号 15K00099
研究機関神戸大学

研究代表者

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

研究分担者 田村 直之  神戸大学, 情報基盤センター, 教授 (60207248)
宋 剛秀  神戸大学, 情報基盤センター, 助教 (00625121)
研究期間 (年度) 2015-04-01 – 2018-03-31
キーワード解集合プログラミング / 制約プログラミング / SAT
研究実績の概要

本研究の目的は,SAT 符号化を用いて,解集合プログラミング (ASP) と制約プログラミング (CP) を融合した制約解集合プログラミング (制約 ASP) を実現することである.具体的な研究テーマは,(A) 制約 ASP 言語に関する研究,(B) 制約 ASP ソルバーの設計・実装,(C) 制約 ASP ソルバーの拡張,(D) 制約 ASP の特長的なアプリケーションの開発,および問題記述例の蓄積の4つである.
本年度は上記の(A)と(B) を完了し(C)と(D)に着手した.その結果,以下に述べる成果を得た.
(A)と(B)については,海外共同研究者・Schaub教授 (ポツダム大学,ドイツ)と協力して制約 ASP 言語の設計,制約 ASP ソルバー clingcon の実装を行い,その成果を(昨年に引き続き)国際ジャーナルに投稿中である.
(C)について,制約充足問題(CPの言語)を SAT に符号化するハイブリッド符号化の研究,SAT 問題の全解を列挙する ALLSAT の研究,制約最適化問題を解くためのインクリメンタル SAT 解法の研究を行った.これらの成果は,国際ジャーナル(2本)と国内ジャーナル(1本)に採択された.また,ハイブリッド符号化とその関連研究について,研究分担者が第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)の発表賞(一般の部)を受賞した.
(D)について,時間割編成とシステム生物学に関する応用研究を行った.これらの成果は,国際ジャーナル(2本)と国際会議(3本)に採択された.さらに,回路の配線問題と親和性の高い多層ナンバーリンクを解く ASP プログラムを開発し,アルゴリズムデザインコンテスト(DAシンポジウム2016に併設)において第2位となり優秀賞を受賞した.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

本研究は交付申請書に記載した「研究実施計画」に照らして順調に進捗している.
最終年度である平成29年度に計画されている(C)の制約 ASP ソルバーの拡張,(D)の制約 ASP の特長的なアプリケーションの開発および問題記述例の蓄積について,その準備状況を述べる.
近年人工知能分野を中心に多目的最適化問題に関する研究開発が活発化している.多目的最適化問題の解は,パレート最適性によって定義され,実問題のもつトレードオフ関係にある多様な解を表現できる.我々は SAT 符号化と極小モデル生成を用いた多目的最適化問題の解法について研究開発を進めており,最近得られた成果を国際会議に投稿中である.(C)については,この研究成果を用いて制約 ASP ソルバーを拡張することで,効率の良い多目的最適化が実現できることが期待できる.
(D)について,複数の評価基準をもつテストケース生成問題の解法について研究開発を進めている.この成果の一部をまとめた論文は,国際会議 LPNMR2017 に採録が決定している.このソフトウェアのテストケース生成については,近年ソフトウェア工学分野を中心に多くの研究開発が進めれている.制約 ASP のソフトウェア工学への応用という観点からも,特長的なアプリケーションとして期待できる.この他にも,特長的なアプリケーションとして,部分グラフ探索,ペトリネットのデッドロック検出などについて研究調査を開始している.

今後の研究の推進方策

最終年度である平成29年度は,(C)の制約 ASP ソルバー拡張,(D)のアプリケーション開発および問題記述例の蓄積を完了する.そして最後に,(D)の問題群を用いて,(B)と(C)で開発したソルバーの総合的な評価を行う.
これまでに,(A)の制約 ASP 言語に関する研究,(B)の制約 ASP ソルバー開発を完了している.(B)では2種類の制約 ASP ソルバー Aspartame と clingconを設計・実装した.Aspartame は SAT 符号化に基づく符号化型ソルバーであり,clingcon は背景論理に基づく SMT 型ソルバーである.本研究の総合的な評価を行う際には,これら2種類のソルバーの長所・短所を詳しく研究調査し明らかにすることが重要である.
(C)では,ハイブリッド符号化,インクリメンタル解法の研究成果,および現在進めている多目的最適化の研究を元に,(B)で開発した2種類の制約 ASP ソルバーを拡張する.これにより,より大規模な制約充足問題および(多目的)制約最適化問題を効率よく求解できるようになることが期待できる.(D)のアプリケーションについては,時間割問題,システム生物学の諸問題,テストケース生成問題,回路の配線問題を中心に研究を進める.
研究代表者・番原と連携研究者・井上の研究拠点が離れているため,4名の研究者全員が参加する研究打合せを年2回開催する.ここでは,アイデア・実現技術の共有を主目的とし,進捗状況の報告,研究計画・方法に関する議論を行う.海外共同研究者はこの研究打合せに年1回参加し,本研究に関連する海外での最新動向の紹介などを通して本研究の推進に寄与する. このような密接な協力体制を整えることによって,研究が当初の計画通りに進まない場合,研究者間で対応策を検討し,研究計画・方法の見直し等を速やかに行えると考えている.

研究成果

(24件)

すべて 2017 2016 その他

すべて 国際共同研究 雑誌論文 学会発表

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

    • 国名
      ドイツ
    • 外国機関名
      ポツダム大学
  • [雑誌論文] 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) ページ: -

    • DOI

      10.1142/S0218213017600053

    • 査読あり / オープンアクセスとしている
  • [雑誌論文] SAT型制約プログラミングシステムと周辺技術2017

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

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

      巻: 34(1) ページ: 67-80

    • DOI

      10.11309/jssst.34.1_67

    • 査読あり / オープンアクセスとしている
  • [雑誌論文] Modeling Delayed Dynamics in Biological Regulatory Networks from Time Series Data2017

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

      Algorithms

      巻: 10(1) ページ: -

    • DOI

      10.3390/a10010008

    • 査読あり / オープンアクセスとしている / 国際共著/国際学会である
  • [雑誌論文] Analyzing Resilience Properties in Oscillatory Biological Systems Using Parametric Model Checking2016

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

      BioSystems

      巻: 149 ページ: 50-58

    • DOI

      10.1016/j.biosystems.2016.09.002

    • 査読あり / 国際共著/国際学会である
  • [雑誌論文] インクリメンタルSAT解法ライブラリとその応用2016

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

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

      巻: 33(4) ページ: 16-29

    • DOI

      10.11309/jssst.33.4_16

    • 査読あり / オープンアクセスとしている
  • [雑誌論文] SAT技術の進化2016

    • 著者名/発表者名
      番原睦則, 鍋島英知
    • 雑誌名

      情報処理

      巻: 57(8) ページ: 704-709

    • 査読あり
  • [雑誌論文] SATとパズル2016

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

      情報処理

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

    • 査読あり
  • [雑誌論文] Implementing Efficient All Solutions SAT Solvers2016

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

      Journal of Experimental Algorithmics

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

    • DOI

      10.1145/2975585

    • 査読あり
  • [雑誌論文] 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

    • 査読あり / オープンアクセスとしている / 国際共著/国際学会である / 謝辞記載あり
  • [雑誌論文] \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

    • 査読あり / オープンアクセスとしている / 国際共著/国際学会である / 謝辞記載あり
  • [雑誌論文] Inference of Delayed Biological Regulatory Networks from Time Series Data2016

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

      Proceedings of the 14th International Conference on Computational Methods in Systems Biology (CMSB 2016)

      巻: 9859 ページ: 30-48

    • DOI

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

    • 査読あり / 国際共著/国際学会である
  • [学会発表] SAT ソルバーの進歩2017

    • 著者名/発表者名
      番原睦則
    • 学会等名
      2017年電子情報通信学会総合大会
    • 発表場所
      名城大学 (愛知県・名古屋市)
    • 年月日
      2017-03-22 – 2017-03-25
    • 招待講演
  • [学会発表] ブール基数制約を経由した擬似ブール制約のSAT符号化法2017

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

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

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

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

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

    • 著者名/発表者名
      宋剛秀,番原睦則,田村直之
    • 学会等名
      第58回プログラミング・シンポジウム
    • 発表場所
      ラフォーレ倶楽部伊東温泉湯の庭(静岡県・伊東市)
    • 年月日
      2017-01-06 – 2017-01-08
  • [学会発表] 解集合プログラミングを用いたナンバーリンクの解法に関する一考察2016

    • 著者名/発表者名
      坡山直樹, 川原征大, 迫龍哉, 番原睦則
    • 学会等名
      DAシンポジウム2016
    • 発表場所
      ゆのくに天祥 (石川県・加賀市)
    • 年月日
      2016-09-14 – 2016-09-16
  • [学会発表] SAT型制約ソルバーを用いた多層ナンバーリンクの解法2016

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

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

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

    • 著者名/発表者名
      迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知
    • 学会等名
      2016年度 人工知能学会全国大会
    • 発表場所
      北九州国際会議場 (福岡県・北九州市)
    • 年月日
      2016-06-06 – 2016-06-09

URL: 

公開日: 2018-01-16  

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

Powered by NII kakenhi