山梨大学
大学院 総合研究部 工学域
電気電子情報工学系(コンピュータ理工学)

顔写真
准教授

鍋島 英知

ナベシマ ヒデトモ
NABESHIMA Hidetomo

経歴

  1. 日本学術振興会 特別研究員 1998/03/31
  2. 山梨大学工学部コンピュータ・メディア工学科 助手 2001/04/01
  3. 山梨大学大学院医学工学総合研究部 助手 2003/04/01
  4. 山梨大学大学院医学工学総合研究部 助教 2007/04/01
  5. 山梨大学大学院医学工学総合研究部 准教授 2009/01/01

学歴

  1. 豊橋技術科学大学 1996/03/01
  2. 豊橋技術科学大学 1998/03/01
  3. 神戸大学 2001/03/01

学位

  1. 博士(工学) 神戸大学

研究分野

  1. 情報学基礎
  2. 知能情報学 人工知能

研究キーワード

  1. 制約充足問題
  2. 人工知能
  3. プランニングとスケジューリング
  4. 知識表現と推論
  5. 結論発見
  6. 命題論理の充足可能性問題 (SAT)
  7. WEB検索隠し味の半自動学習

研究テーマ

  1. 知識表現と自動推論,制約充足処理系の設計・開発

著書

  1. データ構造とアルゴリズム 岩沼 宏治 美濃 英俊 鍋島 英知 山本 泰生 1,2,3章 コロナ社 2018/02/01 978-4339018233 本書は,最近の動向に合わせて,機械学習的考え方,ビッグデータ的考え方,さらには擬似コードとC++実コードによるオブジェクト指向的考え方にも配慮しつつ,通常の学部用教科書としての側面もしっかりと押さえた教科書である。

論文

  1. 研究論文(国際会議プロシーディングス) 共著 Coverage-Based Clause Reduction Heuristics for CDCL Solvers Hidetomo Nabeshima Katsumi Inoue Proceedings of the 20th International Conference Theory and Applications of Satisfiability Testing (SAT 2017) Springer, Cham 10491, 136-144 2017/08/30 1611-3349 10.1007/978-3-319-66263-3 Many heuristics, such as decision, restart, and clause reduction heuristics, are incorporated in CDCL solvers in order to improve performance. In this paper, we focus on learnt clause reduction heuristics, which are used to suppress memory consumption and sustain propagation speed. The reduction heuristics consist of evaluation criteria, for measuring the usefulness of learnt clauses, and a reduction strategy in order to select clauses to be removed based on the criteria. LBD (literals blocks distance) is used as the evaluation criteria in many solvers. For the reduction strategy, we propose a new concise schema based on the coverage ratio of used LBDs. The experimental results show that the proposed strategy can achieve higher coverage than the conventional strategy and improve the performance for both SAT and UNSAT instances.
  2. 研究論文(国際会議プロシーディングス) 共著 Completing Signaling Networks by Abductive Reasoning with Perturbation Experiments Adrien Rougny, Yoshitaka Yamamoto, Hidetomo Nabeshima, Gauvain Bourgne, Anne Poupon, Katsumi Inoue, Christine Froidevaux Late Breaking Papers of the 25th International Conference on Inductive Logic Programming (ILP 2015) CEUR Workshop Proceedings 1636, 95-100 2016
  3. 研究論文(学術雑誌) 共著 インクリメンタルSAT解法ライブラリとその応用 迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳 コンピュータソフトウェア 33/ 4, 16-29 2016 0289-6540 10.11309/jssst.33.4_16
  4. (MISC)総説・解説(学術雑誌) 共著 SAT技術の進化 番原 睦則 , 鍋島 英知 情報処理 57/ 8, 704-709 2016/07
  5. (MISC)総説・解説(学術雑誌) 共著 SATソルバーの最近の進展 鍋島 英知, 岩沼 宏治, 井上 克巳 情報処理 57/ 8, 724-729 2016/07

研究発表

  1. 口頭発表(一般) 決定的ポートフォリオ型並列SATソルバーの待ち時間削減による高速化手法 人工知能学会 第106回 人工知能基本問題研究会 2018/03/16
  2. 口頭発表(招待・特別) 研究室配属問題のCSP符号化手法の検討 第31回人工知能学会全国大会 2017/05/23
  3. 口頭発表(一般) ポートフォリオ型SATソルバーのための分類器の構築手法 人工知能学会 第103回 人工知能基本問題研究会 2017/03/13
  4. 口頭発表(一般) 同順位を含む研究室配属問題のCSPソルバーによる解法の検討 人工知能学会 第103回 人工知能基本問題研究会 2017/03/13
  5. 口頭発表(招待・特別) SAT ソルバーの最近の技術動向 2016年度人工知能学会全国大会 2016/06/06

上記以外の発表の総数

  1. 2016 4 0 4
  2. 2015 3 0 3
  3. 2014 5 0 5
  4. 2013 2 0 2
  5. 2012 3 0 3

知的財産権

  1. 防犯・防災監視システム 特許出願平10-164527 1998/06/12 398029429

受賞

  1. ⼈⼯知能学会研究会優秀賞 同順位を含む研究室配属問題のCSPソルバーによる解法の検討 2017/06/26
  2. 日本ソフトウェア科学会第3回ソフトウェア論文賞 2014/09/08 GlueMiniSat 2.2.5: 単位伝搬を促す学習節の積極的獲得戦略に基づく高速SAT ソルバー
  3. SAT 2013 競技会産業応用部門UNSATクラス準優勝 2013/07/12 命題論理の充足可能性判定(SAT)問題を高速に解くソフトウェアに関する国際競技会 SAT 2013 Competition にて,産業応用部門 UNSAT クラスにて準優勝を果たした
  4. 第18回山梨科学アカデミー奨励賞 2013/05/27 鍋島らは,計算機科学における基本問題の1つである命題論理における充足可能性判定(SAT)と,自動推論の基盤となる一階論理における結論発見に関して,優れたソフトウェアを開発している.前者ではソルバーの性能を競う国際競技会で部門別優勝するなど大きな成果を挙げており,後者では効率的に結論を発見するシステムSOLARを構築し,国内外の様々な研究課題の推論エンジンとして利用されている.
  5. 日本ソフトウェア科学会第28回大会高橋奨励賞 2012/08/23 受賞の対象となった研究発表は「GlueMiniSat2.2.5: 単位伝搬を促す学習節の積極的獲得戦略に基づく高速SATソルバー」であり,情報科学で最も基本的で本質的な組合せ問題である命題論理の充足可能性判定問題 (SAT問題) を高速に解くソルバーを開発したことが顕著な成果として認められた.

学外あるいは所属学部等外の組織との共同研究

  1. 2015/04/01-2016/03/31 国立情報学研究所 分担 クラウド上のソフトウェア最適配置問題の解法 大規模なソフトウェア最適配置問題を効率よく解くために,本研究ではそれを制約最適化問題として定式化し,それを高速なSATソルバーにより解く手法を採用している.この手法の高速化のため,SATソルバーにおける探索ヒューリスティクス等の改良に取り組んだ.提案手法は,既存研究と比較して大幅な高速化を実現している.
  2. 2014/04/01-2015/03/31 国立情報学研究所 分担 分子ネットワーク推論によるGPCR調節機構の解明
  3. 2013/04/01-2014/03/31 国立情報学研究所 分担 分子ネットワークの再構築を目的とする推論技術の高度化 仮説発見器のベースとなる一階述語論理の結論発見器の高速化を達成した.
  4. 2012/05/01-2014/03/31 インスブルック大学・教授・Aart Middeldorp(代表者) 分担 制約充足性判定の書換え理論への導入とソフトウェア検証への応用 SMTソルバの推論エンジンとなるSATソルバの性能向上を達成し,またUNSATコアの高速抽出手法を導入した.
  5. 2012/04/01-2013/03/31 国立情報学研究所 分担 分散環境における結論発見およびSAT/MaxSATに関する研究 高速SATソルバの実現と高速結論発見手続きの実現

所属学協会

  1. Association for Computing Machinery 2012/09
  2. 日本ソフトウェア科学会 2011/11
  3. 電子情報通信学会 2005/04
  4. 人工知能学会 1997/11

学外委員

  1. 人工知能学会人工知能基本問題研究会 幹事 2010/04-2012/03
  2. 情報処理学会 プログラミング研究運営委員会 運営委員 2008/04-2013/03
  3. 電子情報通信学会 人工知能と知識処理研究専門委員会 専門委員 2007/05-2013/05
  4. 電子情報通信学会 人工知能と知識処理研究専門委員会 幹事補佐 2005/05-2007/05