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

2017 年度 実施状況報告書

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

研究課題

研究課題/領域番号 16K16036
研究機関神戸大学

研究代表者

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

研究期間 (年度) 2016-04-01 – 2019-03-31
キーワードSATソルバー / SAT符号化 / 順序符号化 / 対数符号化 / ハイブリッド符号化 / 制約充足問題 / 制約プログラミング
研究実績の概要

近年,SAT問題を解くプログラムであるSATソルバーの飛躍的な進歩にともない,CSPをSAT問題に符号化(SAT符号化)して解くSAT型の制約プログラミング(CP)システムが成功している.本研究の目的は,複数のSAT符号化を変数レベルで融合可能なハイブリッドSAT符号化を実現し,それを実装した高性能なSAT型CPシステムを研究開発することである.本研究の意義は,SAT符号化の新しい方向性を開拓できる点,既存のCPシステムでは求解困難な問題に対して.より高性能な推論基盤を提供できる点である.CPシステムはサッカーのJリーグの対戦スケジュール開発に使われるなど実用性が非常に高く,研究成果の産業分野への応用も期待できる.

平成29年度は研究計画に記載された「(B-2) 解析結果を用いたハイブリッド符号化の自動構成」と「(C) 提案 SAT 型 CP システムの特長的なアプリケーションの研究と開発」に取り組んだ.(B-2) については,自動構成を実装したSAT型制約プログラミングシステムである scop の開発を開始した.(C) については,多目的制約最適化問題に対してハイブリッド符号化を適用する研究に取り組んだ.多目的制約最適化問題では,目的変数を順序符号化し,それ以外の変数を対数符号化するようにハイブリッド符号化を構成した.計算機実験の結果,提案方法を実装したシステムが既存方法を実装したシステムと競争的な結果を示すことが分かった.この研究成果は国際会議 CP2017 で発表した.

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

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

理由

当初の計画通り,平成29年度は研究計画に記載された「(B-2) 解析結果を用いたハイブリッド符号化の自動構成」と「(C) 提案 SAT 型 CP システムの特長的なアプリケーションの研究と開発」を行い成果を得た.また上記課題に関する国際論文誌,国際学会への成果発表を行った.これより本研究課題は概ね順調に進展している.

今後の研究の推進方策

平成29年度について計画していた研究内容は,順調に進めることができた.最終年度も計画通り「(B-2) ハイブリッド符号化の自動構成の研究」と「(C) アプリケーション研究」を行う.

研究成果

(12件)

すべて 2018 2017 その他

すべて 国際共同研究 雑誌論文 学会発表 備考 学会・シンポジウム開催

  • [国際共同研究] アルトワ大学(フランス)

    • 国名
      フランス
    • 外国機関名
      アルトワ大学
  • [雑誌論文] 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

      巻: - ページ: 印刷中

    • DOI

      10.1007/s10479-018-2757-7

    • 査読あり / 国際共著/国際学会である
  • [雑誌論文] 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

    • 査読あり / オープンアクセスとしている
  • [雑誌論文] 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

    • 査読あり / 国際共著/国際学会である
  • [雑誌論文] 解集合プログラミングによるカリキュラムベース・コース時間割編成2017

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

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

      巻: - ページ: 73-88

    • 国際共著/国際学会である
  • [雑誌論文] 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

    • 査読あり / 国際共著/国際学会である
  • [学会発表] ブール基数制約を経由した擬似ブール制約のSAT符号化手法2017

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

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

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

    • 著者名/発表者名
      坡山直樹, 番原睦則, 宋剛秀, 田村直之
    • 学会等名
      人工知能学会全国大会(第31回)
  • [備考] 宋 剛秀 (業績,ソフトウェアへのリンク)

    • URL

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

  • [学会・シンポジウム開催] CRIL-Kobe-Louvain 共同ワークショップ2017

URL: 

公開日: 2018-12-17  

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

Powered by NII kakenhi