充足可能性判定器の高速化に関する研究

• 研究課題/領域番号: 26330248
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: 知能情報学
• 研究機関: 山梨大学
• 研究代表者: 鍋島 英知 山梨大学, 総合研究部, 准教授 (10334848)
• 研究期間 (年度): 2014-04-01 – 2017-03-31
• 研究課題ステータス: 完了 (2016年度)
• 配分額: 4,810千円 (直接経費: 3,700千円、間接経費: 1,110千円); 2016年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円); 2015年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2014年度: 2,600千円 (直接経費: 2,000千円、間接経費: 600千円)
• キーワード: 充足可能性判定問題 / SATソルバー / 充足可能性判定(SAT)問題 / 動的簡単化

研究成果の概要

命題論理の充足可能性問題を解くSATソルバーは，困難な組み合わせ問題を解くための重要な基盤であり，システム検証やスケジューリングなどの様々な分野に応用されている．本研究では，SATソルバーの高速化を目的として，求解中に動的に問題を簡単化する手法や，頑健なヒューリスティクスの構築，並列解法などについて研究開発を行い，これらの手法を用いることで従来手法よりも高速に求解できることを実証した．

研究成果

• [雑誌論文] インクリメンタルSAT解法ライブラリとその応用 (2016)
  • 著者名/発表者名: 迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
  • 雑誌名: コンピュータ ソフトウェア 巻: 33 号: 4 ページ: 4_16-4_29
  • DOI: 10.11309/jssst.33.4_16
  • NAID: 130005290581
  • ISSN: 0289-6540
  • 査読あり / オープンアクセス
• [雑誌論文] Construction of an ROBDD for a PB-Constraint in Band Form and Related Techniques for PB-Solvers (2015)
  • 著者名/発表者名: Masahiko SAKAI and Hidetomo NABESHIMA
  • 雑誌名: IEICE Transactions on Information and Systems 巻: E98.D 号: 6 ページ: 1121-1127
  • DOI: 10.1587/transinf.2014FOP0007
  • NAID: 130005072390
  • ISSN: 0916-8532, 1745-1361
  • 査読あり
• [雑誌論文] Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers (2015)
  • 著者名/発表者名: Masahiko SAKAI, Hidetomo NABESHIMA
  • 雑誌名: IEICE TRANSACTIONS on Information and Systems 巻: E98-D
  • NAID: 130005072390
  • 査読あり
• [学会発表] ポートフォリオ型SATソルバーのための分類器の構築手法 (2017)
  • 著者名/発表者名: 藤江 柊輔，鍋島 英知
  • 学会等名: 人工知能学会 第103回人工知能基本問題研究会
  • 発表場所: 湯布院公民館（大分県）
  • 年月日: 2017-03-13
• [学会発表] 同順位を含む研究室配属問題のCSPソルバーによる解法の検討 (2017)
  • 著者名/発表者名: 藤井 樹，伊藤 靖展，鍋島 英知
  • 学会等名: 人工知能学会 第103回人工知能基本問題研究会
  • 発表場所: 湯布院公民館（大分県）
  • 年月日: 2017-03-13
• [学会発表] SAT ソルバーの最近の技術動向 (2016)
  • 著者名/発表者名: 鍋島 英知
  • 学会等名: 第30回人工知能学会全国大会
  • 発表場所: 北九州国際会議場（大分県）
  • 年月日: 2016-06-06
  • 招待講演
• [学会発表] SAT型制約ソルバーによるナンバーリンクの解法とその評価 (2016)
  • 著者名/発表者名: 迫 龍哉，川原 征大，宋 剛秀，番原 睦則，田村 直之，鍋島 英知
  • 学会等名: 第30回人工知能学会全国大会
  • 発表場所: 北九州国際会議場（大分県）
  • 年月日: 2016-06-06
• [学会発表] CDCLソルバーにおけるZDDを利用した節圧縮表現の導入 (2016)
  • 著者名/発表者名: 後藤 優也，鍋島 英知
  • 学会等名: 第30回人工知能学会全国大会
  • 発表場所: 北九州国際会議場（大分県）
  • 年月日: 2016-06-06
• [学会発表] クラウド上のソフトウェア要素最適配置問題の解法 (2016)
  • 著者名/発表者名: 田村 直之, 井上 克巳, 鍋島 英知, 番原 睦則, 宋 剛秀
  • 学会等名: 人工知能学会 第100回人工知能基本問題研究会
  • 発表場所: 熊本市民会館(熊本県熊本市)
  • 年月日: 2016-03-27
• [学会発表] SATソルバーの安定性向上のための粗な初期探索手法の検討と提案 (2015)
  • 著者名/発表者名: 三神 直彬，鍋島 英知
  • 学会等名: 第29回人工知能学会全国大会
  • 発表場所: 公立はこだて未来大学(北海道函館市)
  • 年月日: 2015-05-30
• [学会発表] CDCLソルバーのための軽量動的簡単化手法 (2015)
  • 著者名/発表者名: 杉本 拓也，鍋島 英知
  • 学会等名: 人工知能学会 第97回人工知能基本問題研究会
  • 発表場所: 別府国際コンベンションセンター（大分県・別府市）
  • 年月日: 2015-03-22 – 2015-03-23
• [学会発表] CDCLソルバーにおける学習節の深さに基づく節管理戦略 (2015)
  • 著者名/発表者名: 横前 菜々子，鍋島 英知
  • 学会等名: 人工知能学会 第97回人工知能基本問題研究会
  • 発表場所: 別府国際コンベンションセンター（大分県・別府市）
  • 年月日: 2015-03-22 – 2015-03-23
• [学会発表] SAT変換手法における充足不能コアの抽出 (2015)
  • 著者名/発表者名: 渡辺 大樹，鍋島 英知
  • 学会等名: 人工知能学会 第97回人工知能基本問題研究会
  • 発表場所: 別府国際コンベンションセンター（大分県・別府市）
  • 年月日: 2015-03-22 – 2015-03-23
• [学会発表] CDCL ソルバーのための軽量動的包摂検査 (2014)
  • 著者名/発表者名: 杉本 拓也，鍋島 英知
  • 学会等名: 第28回人工知能学会全国大会
  • 発表場所: ひめぎんホール（愛媛県・松山市）
  • 年月日: 2014-05-12 – 2014-05-15
• [学会発表] 大規模SAT問題の求解のための緩和解法の検討と提案 (2014)
  • 著者名/発表者名: 三神 直彬，鍋島 英知
  • 学会等名: 第28回人工知能学会全国大会
  • 発表場所: ひめぎんホール（愛媛県・松山市）
  • 年月日: 2014-05-12 – 2014-05-15
• [備考] GlueMiniSat ホームページ
  • URL: http://glueminisat.nabelab.org/
• [備考] GlueMiniSat
  • URL: http://glueminisat.nabelab.org/