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

2015 年度 実施状況報告書

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)を中心に研究開発を進めた.海外共同研究者・Schaub教授 (ポツダム大学,ドイツ)と協力して制約ASP言語の設計を行い,制約ASPソルバーclingconを実装した.この研究成果については,国際ジャーナル論文に投稿中である.また,制約充足問題(CPの言語)をASPに符号化し,既存のASPソルバーで求解するCPソルバーAspartameを実装した.このAspartameは,制約充足問題をSATに符号化する順序符号化法を応用したものであり,既存のSATベースの高速CPソルバーSugarとほぼ同等の性能を実現した.この研究成果については, 国際会議LPNMR2015で発表した.さらに,制約充足問題をSATに符号化する新しい方法として,順序符号化法と対数符号化法を融合したハイブリッド符号化を提案した.このハイブリッド符号化は,順序符号化法と比較してより大規模な制約充足問題を取り扱えることから,今後のAspartameの実装・拡張において重要な役割を果たすことが期待できる.この研究成果については,国際会議ICTAI2015で発表した.

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

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

理由

本研究は交付申請書に記載した「研究実施計画」に照らして順調に進捗している.(B)の制約ASPソルバーの設計・実装には,大きく分けて「SMT型」と「符号化型」の2つがある.現時点でどちらの方法が優れているかの判断は難しい.そのため,本研究では両者の長所・短所を詳しく研究調査し,両者のハイブリッド方式も視野に入れつつ研究開発を進めることが重要となる.実際,本年度開発した制約ASPソルバーclingconは「SMT型」,CPソルバーAspartameは「符号化型」を採用している.新しく考案した制約充足問題からSATへのハイブリッド符号化法は,「符号化型」のための最適化技術として有用である.
次年度以降に計画されている(C)制約ASPソルバーの拡張,(D) 制約ASPの特長的なアプリケーションの開発および問題記述例の蓄積について,その準備として以下の研究を行った.「組合せテストケース生成問題に対する制約解集合プログラミングの適用」と題する研究発表を2015年度人工知能学会全国大会(第29回)で行い,全国大会優秀賞を受賞した.また,制約最適化問題をSATソルバーのインクリメンタル解法を用いて効率良く解く方法について研究開発を行った.この研究成果は,日本ソフトウェア科学会論文誌コンピュータソフトウェアに採録が決定している.さらに,開発したソルバーは,アルゴリズムデザインコンテスト(情報処理学会DAシンポジウム2015の企画イベント)において,第1位となり最優秀賞を受賞した.

今後の研究の推進方策

中間年度である平成28年度は,(A)の制約ASP言語に関する研究を終え,(B)の制約ASPソルバー開発を完成する.また,(C)の制約ASPソルバー拡張を開始するとともに,(D)の制約ASP記述例の蓄積についても着手する.(C)では,インクリメンタル解法,ヒューリスティクス埋込み機能等の高度なASP解法を利用することにより,(B)で開発した制約ASPソルバーを拡張する.この拡張により,モデル検査をはじめ近年様々な分野に応用されているCEGARループ,CPの分野でこれまで研究されてきた変数選択および探索ヒューリスティクスなどを,簡潔に記述できるようになることが期待できる.
最終年度である平成29年度は,(C)の制約 ASP ソルバー拡張,(D)のアプリケーション開発および問題記述例の蓄積を完成する.そして最後に,(D)の問題群を用いて,(B), (C) で開発したソルバーの総合的な評価を行う.(D)のアプリケーションとしては,時間割問題,ソフトウェアのテストケース生成問題を中心に研究を進める.特に,(C)で拡張された制約ASPソルバーを用いることにより,時間割問題に対して,主にオペレーションズ・リサーチ分野で研究されてきた様々なヒューリスティクスを利用することが期待できる.
研究代表者・番原と連携研究者・井上の研究拠点が離れているため,4名の研究者全員が参加する研究打合せを年2回開催する.ここでは,アイデア・実現技術の共有を主目的とし,進捗状況の報告,研究計画・方法に関する議論を行う.海外共同研究者はこの研究打合せに年1回参加し,本研究に関連する海外での最新動向の紹介などを通して本研究の推進に寄与する. このような密接な協力体制を整えることによって,研究が当初の計画通りに進まない場合,研究者間で対応策を検討し,研究計画・方法の見直し等を速やかに行えると考えている.

次年度使用額が生じた理由

計画当初,海外共同研究者Schaub教授 (ポツダム大学,ドイツ)との研究打合せを神戸で予定していたが,本年度はポツダム大学で開催した.そのため,Schaub教授の講演謝金が不要となり,次年度使用額が生じた.

次年度使用額の使用計画

次年度以降の研究推進のために必要となるソフトウェア開発用パソコンの購入および旅費として使用する.

研究成果

(16件)

すべて 2016 2015 その他

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

  • [国際共同研究] University of Potsdam(ドイツ)

    • 国名
      ドイツ
    • 外国機関名
      University of Potsdam
  • [国際共同研究] Aalto University(フィンランド)

    • 国名
      フィンランド
    • 外国機関名
      Aalto University
  • [国際共同研究] University of Ferrara(イタリア)

    • 国名
      イタリア
    • 外国機関名
      University of Ferrara
  • [国際共同研究] INRIA Rennes(フランス)

    • 国名
      フランス
    • 外国機関名
      INRIA Rennes
  • [雑誌論文] 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

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

    • 査読あり / 国際共著/国際学会である
  • [学会発表] クラウド上のソフトウェア要素最適配置問題の解法2016

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

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

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

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

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

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

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

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

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

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

URL: 

公開日: 2017-01-06  

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

Powered by NII kakenhi