鍋島 英知

J-GLOBALへ         更新日: 18/11/20 03:27
 
アバター
研究者氏名
鍋島 英知
 
ナベシマ ヒデトモ
URL
http://www.nabelab.org/
所属
山梨大学
部署
大学院 総合研究部 工学域電気電子情報工学系(コンピュータ理工学)
職名
准教授
学位
博士(工学)(神戸大学)
科研費研究者番号
10334848

研究分野

 
 

経歴

 
2001年4月
   
 
山梨大学工学部コンピュータ・メディア工学科 助手
 
2003年4月
   
 
山梨大学大学院医学工学総合研究部 助手
 
2007年4月
   
 
山梨大学大学院医学工学総合研究部 助教
 
2009年1月
   
 
山梨大学大学院医学工学総合研究部 准教授
 

受賞

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

Misc

 
SAT技術の進化
番原 睦則 , 鍋島 英知
情報処理   57(8) 704-709   2016年7月
SATソルバーの最近の進展
鍋島 英知, 岩沼 宏治, 井上 克巳
情報処理   57(8) 724-729   2016年7月
岩沼宏治,鍋島英知,井上克巳
コンピュータソフトウェア   28(4) 282-305   2011年
SAT によるプランニングとスケジューリング
鍋島 英知
人工知能学会誌   25(1) 114-121   2010年
SMT:個別理論を取り扱うSAT 技術
岩沼 宏治,鍋島 英知
人工知能学会誌   25(1) 86-95   2010年

書籍等出版物

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

講演・口頭発表等

 
決定的ポートフォリオ型並列SATソルバーの待ち時間削減による高速化手法
後藤 優也, 鍋島 英知
人工知能学会 第106回 人工知能基本問題研究会   2018年3月16日   人工知能学会
研究室配属問題のCSP符号化手法の検討 [招待有り]
藤井 樹, 伊藤 靖展, 鍋島 英知
第31回人工知能学会全国大会   2017年5月23日   人工知能学会
ポートフォリオ型SATソルバーのための分類器の構築手法
藤江 柊輔, 鍋島 英知
人工知能学会 第103回 人工知能基本問題研究会   2017年3月13日   人工知能学会
同順位を含む研究室配属問題のCSPソルバーによる解法の検討
藤井 樹, 伊藤 靖展, 鍋島 英知
人工知能学会 第103回 人工知能基本問題研究会   2017年3月13日   人工知能学会
SAT ソルバーの最近の技術動向 [招待有り]
鍋島 英知
2016年度人工知能学会全国大会   2016年6月6日   人工知能学会

論文

 
Hidetomo Nabeshima Katsumi Inoue
Proceedings of the 20th International Conference Theory and Applications of Satisfiability Testing (SAT 2017)   10491 136-144   2017年8月   [査読有り]
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 consump...
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)   1636 95-100   2016年   [査読有り]
迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
コンピュータソフトウェア   33(4) 16-29   2016年   [査読有り]
Masahiko Sakai Hidetomo Nabeshima
IEICE TRANSACTIONS on Information and Systems   E98-D 1121-1127   2015年6月   [査読有り]
Hidetomo Nabeshima,Koji Iwanuma,Katsumi Inoue
Proceedings of IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI 2013),   987-995   2013年11月   [査読有り]

学歴

 
 
 - 
2001年3月
神戸大学