高速結論発見器の実用化に関する研究

• 研究課題/領域番号: 23700164
• 研究種目: 若手研究(B)
• 配分区分: 基金
• 研究分野: 知能情報学
• 研究機関: 山梨大学
• 研究代表者: 鍋島 英知 山梨大学, 医学工学総合研究部, 准教授 (10334848)
• 研究期間 (年度): 2011 – 2013
• 研究課題ステータス: 完了 (2013年度)
• 配分額: 4,290千円 (直接経費: 3,300千円、間接経費: 990千円); 2013年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2012年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2011年度: 2,730千円 (直接経費: 2,100千円、間接経費: 630千円)
• キーワード: 結論発見 / 仮説発見 / 一階述語論理 / 命題論理 / 推論システム / 分割統治

研究概要

一階述語論理の結論発見器であるSOLARのスケーラビリティ向上のため，SOLタブロー計算法の分轄統治法の考案や，最良優先探索に基づく新しい結論発見器の開発と各種の枝刈り技術の導入，SAT技術に基づく命題論理版結論発見器の試作，その推論エンジンとなるSATソルバーの性能改善等に取り組み，従来のSOLARを超える性能を獲得し，SATソルバーは2011年，2013年のSAT競技会の応用UNSAT部門においてそれぞれ優勝・2位を獲得するなどの成果を得た．

研究成果

• [雑誌論文] Completing causal networks by meta-level abduction (2013)
  • 著者名/発表者名: K. Inoue, A. Doncescu, H. Nabeshima
  • 雑誌名: Machine Learning 巻: Vol.91, Issue 2 ページ: 239-277
  • 査読あり
• [雑誌論文] On-The-Fly Lazy Clause Simplification based on Binary Resolvents (2013)
  • 著者名/発表者名: H. Nabeshima, K. Iwanuma, K. Inoue
  • 雑誌名: Proc. of IEEE 25^<th> International Conference on Tools with Artificial Intelligence (ICTAI 2013) ページ: 987-995
  • 査読あり
• [雑誌論文] Completing causal networks by meta-level abduction (2013)
  • 著者名/発表者名: Katsumi Inoue, Andrei Doncescu, Hidetomo Nabeshima
  • 雑誌名: Machine Learning 巻: Volume 91, Issue 2 号: 2 ページ: 239-277
  • DOI: 10.1007/s10994-013-5341-z
  • 査読あり
• [雑誌論文] GlueMiniSat2.2.5 : 単位伝搬を促す学習節の積極的獲得戦略に基づく高速SAT ソルバー (2012)
  • 著者名/発表者名: 鍋島 英知, 岩沼 宏治, 井上 克巳
  • 雑誌名: コンピュータソフトウェア 巻: Vol.29, No.4 ページ: 146-160
  • NAID: 130004549290
  • 査読あり
• [雑誌論文] GlueMiniSat 2.2.5: 単位伝搬を促す学習節の積極的獲得戦略に基づく高速SATソルバー (2012)
  • 著者名/発表者名: 鍋島英知
  • 雑誌名: コンピュータ ソフトウェア 巻: 29 号: 4 ページ: 4_146-4_160
  • DOI: 10.11309/jssst.29.4_146
  • NAID: 130004549290
  • ISSN: 0289-6540
  • 査読あり
• [雑誌論文] GlueMiniSat 2.2.5：単位伝播を促す学習節の積極的獲得戦略に基づく高速SAT ソルバー (2012)
  • 著者名/発表者名: 鍋島英知，岩沼宏治，井上克巳
  • 雑誌名: コンピュータソフトウェア 巻: 未定
  • 査読あり
• [雑誌論文] Hypothesizing about Causal Networks with Positive and Negative Effects by Meta-level Abduction (2011)
  • 著者名/発表者名: K. Inoue, A. Doncescu, H. Nabeshima
  • 雑誌名: Inductive Logic Programming : Revised Papers from the 20th International Conference (ILP'10) 巻: Vol.6489 ページ: 114-129
  • 査読あり
• [雑誌論文] 一階論理上の等号推論 : 理論と実際 (2011)
  • 著者名/発表者名: 岩沼 宏治,鍋島 英知,井上 克巳
  • 雑誌名: コンピュータソフトウェア 巻: Vol.28,No.4 ページ: 282-305
  • NAID: 130004549242
  • 査読あり
• [雑誌論文] Hypothesizing about Causal Networks with Positive and Negative Effects by Meta-Level Abduction (2011)
  • 著者名/発表者名: Katsumi Inoue, Andrei Doncescu, Hidetomo Nabeshima
  • 雑誌名: Inductive Logic Programming : Revised Papers from the 20th International Conference (ILP'10), Lecture Notes in Artificial Intelligence 巻: 6489 ページ: 114-129
  • DOI: 10.1007/978-3-642-21295-6_15
  • ISBN: 9783642212949, 9783642212956
  • 査読あり
• [雑誌論文] 一階論理上の等号推論：理論と実際 (2011)
  • 著者名/発表者名: 岩沼 宏治，鍋島 英知，井上 克巳
  • 雑誌名: コンピュータソフトウェア 巻: Vol. 28, No.4 ページ: 282-305
  • NAID: 130004549242
  • 査読あり
• [学会発表] Lazy Extension for SOL tableau calculus (2013)
  • 著者名/発表者名: H. Nabeshima
  • 学会等名: The 5th JFLI-NII-LRI Workshop on Formal Approaches for Modeling and Analyzing Biological Networks
  • 発表場所: LRI(フランス)
  • 年月日: 2013-10-09
• [学会発表] 最新 SAT ソルバーへの充足不能コア抽出手法の実装 (2013)
  • 著者名/発表者名: 渡辺 大樹,鍋島 英知
  • 学会等名: 第27回人工知能学会全国大会
  • 発表場所: 富山国際会議場(富山県)
  • 年月日: 2013-06-05
• [学会発表] 拡張融合法に基づく次世代SAT ソルバーの試作 (2013)
  • 著者名/発表者名: 森 淳,鍋島 英知
  • 学会等名: 第27回人工知能学会全国大会
  • 発表場所: 富山国際会議場(富山県)
  • 年月日: 2013-06-05
• [学会発表] On-The-Fly Lazy Clause Simplification based on Binary Resolvents (2013)
  • 著者名/発表者名: Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue
  • 学会等名: IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI 2013)
  • 発表場所: Virginia, USA
• [学会発表] 最新SATソルバーへの充足不能コア抽出手法の実装 (2013)
  • 著者名/発表者名: 渡辺 大樹，鍋島 英知
  • 学会等名: 第27回人工知能学会全国大会
  • 発表場所: 富山国際会議場
• [学会発表] 拡張融合法に基づく次世代SATソルバーの試作 (2013)
  • 著者名/発表者名: 森 淳，鍋島 英知
  • 学会等名: 第27回人工知能学会全国大会
  • 発表場所: 富山国際会議場
• [学会発表] 高速SATソルバーの実装と理論 (2013)
  • 著者名/発表者名: 鍋島英知
  • 学会等名: 第15回プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 東山温泉御宿東鳳（福島県会津若松市）
  • 招待講演
• [学会発表] A Best-First Search Strategy for SOL Tableau Calculus (2012)
  • 著者名/発表者名: H. Nabeshima
  • 学会等名: The 4th JFLI-LRI-NII Workshop on Consequence Finding and Satisfiability Testing in Distributed Environments and Systems Biology
  • 発表場所: LRI(フランス)
  • 年月日: 2012-11-19
• [学会発表] 結論発見システム SOLAR の分割統治法による高速化 (2012)
  • 著者名/発表者名: 寄特 勇紀,鍋島 英知
  • 学会等名: 第26回人工知能学会全国大会
  • 発表場所: 山口県教育会館(山口県)
  • 年月日: 2012-06-12
• [学会発表] 高速充足可能性判定器を用いた命題論理の結論発見器の実装 (2012)
  • 著者名/発表者名: 村松 匠,鈴木 健士郎,鍋島 英知,岩沼 宏治
  • 学会等名: 第26回人工知能学会全国大会
  • 発表場所: 山口県教育会館(山口県)
  • 年月日: 2012-06-12
• [学会発表] 学習節評価尺度LBD に基づく並列SAT ソルバーの提案 (2012)
  • 著者名/発表者名: 大橋 弘幸,鍋島 英知
  • 学会等名: 第26回人工知能学会全国大会
  • 発表場所: 山口県教育会館(山口県)
  • 年月日: 2012-06-12
• [学会発表] 高速SAT ソルバーの実装と理論 (2012)
  • 著者名/発表者名: 鍋島 英知
  • 学会等名: 第15回プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 御宿東鳳(福島県)
  • 年月日: 2012-03-05
  • 招待講演
• [学会発表] 充足可能性判定器に基づく命題論理の結論発見器の提案 (2012)
  • 著者名/発表者名: 鈴木 健士郎,鍋島 英知,岩沼 宏治
  • 学会等名: 第85回人工知能学会人工知能基本問題研究会
  • 発表場所: KKR 下呂しらさぎ(岐阜県)
  • 年月日: 2012-02-03
• [学会発表] SAT ソルバーの探索戦略効率化に向けた合理的尺度の導入検証 (2012)
  • 著者名/発表者名: 村松 匠,鍋島 英知
  • 学会等名: 第85回人工知能学会人工知能基本問題研究会
  • 発表場所: KKR 下呂しらさぎ(岐阜県)
  • 年月日: 2012-02-03
• [学会発表] SOL タブロー計算法の分割統治アルゴリズムの検討 (2012)
  • 著者名/発表者名: 寄特 勇紀,鍋島 英知
  • 学会等名: 第85回人工知能学会人工知能基本問題研究会
  • 発表場所: KKR 下呂しらさぎ(岐阜県)
  • 年月日: 2012-02-03
• [学会発表] 結論発見システム SOLAR の分割統治法による高速化 (2012)
  • 著者名/発表者名: 寄特勇紀，鍋島英知
  • 学会等名: 第26回人工知能学会全国大会
  • 発表場所: 山口県教育会館（山口県山口市）
• [学会発表] 高速充足可能性判定器を用いた命題論理の結論発見器の実装 (2012)
  • 著者名/発表者名: 村松匠，鈴木健士郎，鍋島英知，岩沼宏治
  • 学会等名: 第26回人工知能学会全国大会
  • 発表場所: 山口県教育会館（山口県山口市）
• [学会発表] 学習節評価尺度LBDに基づく並列SATソルバーの提案 (2012)
  • 著者名/発表者名: 大橋弘幸，鍋島英知
  • 学会等名: 第26回人工知能学会全国大会
  • 発表場所: 山口県教育会館（山口県山口市）
• [学会発表] 充足可能性判定器に基づく命題論理の結論発見器の提案 (2012)
  • 著者名/発表者名: 鈴木 健士郎，鍋島 英知，岩沼 宏治
  • 学会等名: 第85回人工知能学会人工知能基本問題研究会
  • 発表場所: 下呂交流会館（岐阜県）
• [学会発表] SATソルバーの探索戦略効率化に向けた合理的尺度の導入検証 (2012)
  • 著者名/発表者名: 村松 匠，鍋島 英知
  • 学会等名: 第85回人工知能学会人工知能基本問題研究会
  • 発表場所: 下呂交流会館（岐阜県）
• [学会発表] SOLタブロー計算法の分割統治アルゴリズムの検討 (2012)
  • 著者名/発表者名: 寄特 勇紀，鍋島 英知
  • 学会等名: 第85回人工知能学会人工知能基本問題研究会
  • 発表場所: 下呂交流会館（岐阜県）
• [学会発表] 局所対称性除去による CDCL ソルバーの効率改善に向けて (2011)
  • 著者名/発表者名: 金澤 潤二,鍋島 英知
  • 学会等名: 第84回人工知能学会人工知能基本問題研究会
  • 発表場所: 慶応義塾大学
  • 年月日: 2011-12-16
• [学会発表] Scalability Improvement of SOL Tableau Calculus based on a Divide-and-Conquer Strategy (2011)
  • 著者名/発表者名: H. Nabeshima, K. Iwanuma, K. Inoue
  • 学会等名: The 3rd LRI-NII Collaborative Meeting on Distributed Reasoning and Problem Decomposition
  • 発表場所: LRI(フランス)
  • 年月日: 2011-10-31
• [学会発表] 局所対称性除去によるCDCL ソルバーの効率化手法の検討 (2011)
  • 著者名/発表者名: 金澤 潤二,鍋島 英知
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 沖縄産業支援センター(沖縄県)
  • 年月日: 2011-09-27
• [学会発表] SOL タブロー計算法に基づく命題論理の充足可能性判定器の実現 (2011)
  • 著者名/発表者名: 鈴木 健士郎, 鍋島 英知
  • 学会等名: 第25回人工知能学会全国大会
  • 発表場所: いわて県民情報交流センター(岩手県)
  • 年月日: 2011-06-03
• [学会発表] ポートフォリオ型戦略の導入による結論発見システムSOLAR の効率改善 (2011)
  • 著者名/発表者名: 村松 匠, 鍋島 英知
  • 発表場所: いわて県民情報交流センター(岩手県)
  • 年月日: 2011-06-02
• [学会発表] 結論発見手続きSOL タブロー計算法の分割統治法に基づく効率化 (2011)
  • 著者名/発表者名: 寄特 勇紀, 鍋島 英知
  • 学会等名: 第25回人工知能学会全国大会
  • 発表場所: いわて県民情報交流センター(岩手県)
  • 年月日: 2011-06-01
• [学会発表] 局所対称性除去による CDCL ソルバーの効率改善に向けて (2011)
  • 著者名/発表者名: 金澤 潤二，鍋島 英知
  • 学会等名: 第84回人工知能学会人工知能基本問題研究会
  • 発表場所: 慶応義塾大学 日吉キャンパス（神奈川県）
• [学会発表] GlueMiniSat 2.2.5：単位伝播を促す学習節の積極的獲得戦略に基づく高速SAT ソルバー (2011)
  • 著者名/発表者名: 鍋島 英知，岩沼 宏治，井上 克巳
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 沖縄産業支援センター（沖縄県）
• [学会発表] 局所対称性除去によるCDCLソルバーの効率化手法の検討 (2011)
  • 著者名/発表者名: 金澤 潤二，鍋島 英知
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 沖縄産業支援センター（沖縄県）
• [学会発表] SOL タブロー計算法に基づく命題論理の充足可能性判定器の実現 (2011)
  • 著者名/発表者名: 鈴木 健士郎, 鍋島 英知
  • 学会等名: 第25回人工知能学会全国大会
  • 発表場所: アイーナ いわて県民情報交流センター（岩手県）
• [学会発表] 結論発見手続き SOL タブロー計算法の分割統治法に基づく効率化 (2011)
  • 著者名/発表者名: 寄特 勇紀, 鍋島 英知
  • 学会等名: 第25回人工知能学会全国大会
  • 発表場所: アイーナ いわて県民情報交流センター（岩手県）
• [学会発表] ポートフォリオ型戦略の導入による結論発見システム SOLAR の効率改善 (2011)
  • 著者名/発表者名: 村松 匠, 鍋島 英知
  • 学会等名: 第25回人工知能学会全国大会
  • 発表場所: アイーナ いわて県民情報交流センター（岩手県）
• [学会発表] 一般双対化問題における 冗長節生成の抑制法とその評価 (2011)
  • 著者名/発表者名: 山本 泰生，鍋島 英知，岩沼 宏治
  • 学会等名: 第25回人工知能学会全国大会
  • 発表場所: アイーナ いわて県民情報交流センター（岩手県）
• [備考] 結論発見システム SOLAR
  • URL: http://solar.nabelab.org/
• [備考] 命題論理の充足可能性判定器 GlueMiniSat
  • URL: http://glueminisat.nabelab.org/
• [備考] 結論発見システム SOLAR
  • URL: http://solar.nabelab.org/
• [備考] 命題論理の充足可能性判定器 GlueMiniSat
  • URL: http://glueminisat.nabelab.org/
• [備考] 結論発見システム SOLAR
  • URL: http://solar.nabelab.org/
• [備考] 命題論理の充足可能性判定器 GlueMiniSat
  • URL: http://glueminisat.nabelab.org/
• [備考]
  • URL: http://solar.nabelab.org/
• [備考]
  • URL: http://glueminisat.nabelab.org/