• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

A study on a practical consequence finding system

Research Project

Project/Area Number 23700164
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeMulti-year Fund
Research Field Intelligent informatics
Research InstitutionUniversity of Yamanashi

Principal Investigator

NABESHIMA Hidetomo  山梨大学, 医学工学総合研究部, 准教授 (10334848)

Project Period (FY) 2011 – 2013
Project Status Completed (Fiscal Year 2013)
Budget Amount *help
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2013: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2012: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2011: ¥2,730,000 (Direct Cost: ¥2,100,000、Indirect Cost: ¥630,000)
Keywords結論発見 / 仮説発見 / 一階述語論理 / 命題論理 / 推論システム / 分割統治
Research Abstract

SOLAR is a first-order consequence finding system. To improve the scalability, we proposed a divide-and-conquer strategy for SOL tableau calculus, developed a new consequence finding system based on best-first search, and introduced various kinds of the pruning techniques for the system. For propositional cases, we developed a prototype of a consequence finding system based on SAT technologies. The new first-order SOLAR system showed superior performance compared to the old one, and the developed SAT solver, called GlueMiniSat, which is used as a inference engine of the propositional system, got 1st and 2nd places of SAT 2011 and 2013 competitions in Applications UNSAT category, respectively.

Report

(4 results)
  • 2013 Annual Research Report   Final Research Report ( PDF )
  • 2012 Research-status Report
  • 2011 Research-status Report
  • Research Products

    (52 results)

All 2013 2012 2011 Other

All Journal Article (10 results) (of which Peer Reviewed: 10 results) Presentation (34 results) (of which Invited: 2 results) Remarks (8 results)

  • [Journal Article] Completing causal networks by meta-level abduction2013

    • Author(s)
      K. Inoue, A. Doncescu, H. Nabeshima
    • Journal Title

      Machine Learning

      Volume: Vol.91, Issue 2 Pages: 239-277

    • Related Report
      2013 Final Research Report
    • Peer Reviewed
  • [Journal Article] On-The-Fly Lazy Clause Simplification based on Binary Resolvents2013

    • Author(s)
      H. Nabeshima, K. Iwanuma, K. Inoue
    • Journal Title

      Proc. of IEEE 25^<th> International Conference on Tools with Artificial Intelligence (ICTAI 2013)

      Pages: 987-995

    • Related Report
      2013 Final Research Report
    • Peer Reviewed
  • [Journal Article] Completing causal networks by meta-level abduction2013

    • Author(s)
      Katsumi Inoue, Andrei Doncescu, Hidetomo Nabeshima
    • Journal Title

      Machine Learning

      Volume: Volume 91, Issue 2 Issue: 2 Pages: 239-277

    • DOI

      10.1007/s10994-013-5341-z

    • Related Report
      2013 Annual Research Report 2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] GlueMiniSat2.2.5 : 単位伝搬を促す学習節の積極的獲得戦略に基づく高速SAT ソルバー2012

    • Author(s)
      鍋島 英知, 岩沼 宏治, 井上 克巳
    • Journal Title

      コンピュータソフトウェア

      Volume: Vol.29, No.4 Pages: 146-160

    • NAID

      130004549290

    • Related Report
      2013 Final Research Report
    • Peer Reviewed
  • [Journal Article] GlueMiniSat 2.2.5: A Fast SAT Solver with An Aggressive Acquiring Strategy of Glue Clauses2012

    • Author(s)
      鍋島英知
    • Journal Title

      Computer Software

      Volume: 29 Issue: 4 Pages: 4_146-4_160

    • DOI

      10.11309/jssst.29.4_146

    • NAID

      130004549290

    • ISSN
      0289-6540
    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] GlueMiniSat 2.2.5:単位伝播を促す学習節の積極的獲得戦略に基づく高速SAT ソルバー2012

    • Author(s)
      鍋島英知,岩沼宏治,井上克巳
    • Journal Title

      コンピュータソフトウェア

      Volume: 未定

    • Related Report
      2011 Research-status Report
    • Peer Reviewed
  • [Journal Article] Hypothesizing about Causal Networks with Positive and Negative Effects by Meta-level Abduction2011

    • Author(s)
      K. Inoue, A. Doncescu, H. Nabeshima
    • Journal Title

      Inductive Logic Programming : Revised Papers from the 20th International Conference (ILP'10)

      Volume: Vol.6489 Pages: 114-129

    • Related Report
      2013 Final Research Report
    • Peer Reviewed
  • [Journal Article] 一階論理上の等号推論 : 理論と実際2011

    • Author(s)
      岩沼 宏治,鍋島 英知,井上 克巳
    • Journal Title

      コンピュータソフトウェア

      Volume: Vol.28,No.4 Pages: 282-305

    • NAID

      130004549242

    • Related Report
      2013 Final Research Report
    • Peer Reviewed
  • [Journal Article] Hypothesizing about Causal Networks with Positive and Negative Effects by Meta-Level Abduction2011

    • Author(s)
      Katsumi Inoue, Andrei Doncescu, Hidetomo Nabeshima
    • Journal Title

      Inductive Logic Programming : Revised Papers from the 20th International Conference (ILP'10), Lecture Notes in Artificial Intelligence

      Volume: 6489 Pages: 114-129

    • DOI

      10.1007/978-3-642-21295-6_15

    • ISBN
      9783642212949, 9783642212956
    • Related Report
      2011 Research-status Report
    • Peer Reviewed
  • [Journal Article] 一階論理上の等号推論:理論と実際2011

    • Author(s)
      岩沼 宏治,鍋島 英知,井上 克巳
    • Journal Title

      コンピュータソフトウェア

      Volume: Vol. 28, No.4 Pages: 282-305

    • NAID

      130004549242

    • Related Report
      2011 Research-status Report
    • Peer Reviewed
  • [Presentation] Lazy Extension for SOL tableau calculus2013

    • Author(s)
      H. Nabeshima
    • Organizer
      The 5th JFLI-NII-LRI Workshop on Formal Approaches for Modeling and Analyzing Biological Networks
    • Place of Presentation
      LRI(フランス)
    • Year and Date
      2013-10-09
    • Related Report
      2013 Final Research Report
  • [Presentation] 最新 SAT ソルバーへの充足不能コア抽出手法の実装2013

    • Author(s)
      渡辺 大樹,鍋島 英知
    • Organizer
      第27回人工知能学会全国大会
    • Place of Presentation
      富山国際会議場(富山県)
    • Year and Date
      2013-06-05
    • Related Report
      2013 Final Research Report
  • [Presentation] 拡張融合法に基づく次世代SAT ソルバーの試作2013

    • Author(s)
      森 淳,鍋島 英知
    • Organizer
      第27回人工知能学会全国大会
    • Place of Presentation
      富山国際会議場(富山県)
    • Year and Date
      2013-06-05
    • Related Report
      2013 Final Research Report
  • [Presentation] On-The-Fly Lazy Clause Simplification based on Binary Resolvents2013

    • Author(s)
      Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue
    • Organizer
      IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI 2013)
    • Place of Presentation
      Virginia, USA
    • Related Report
      2013 Annual Research Report
  • [Presentation] 最新SATソルバーへの充足不能コア抽出手法の実装2013

    • Author(s)
      渡辺 大樹,鍋島 英知
    • Organizer
      第27回人工知能学会全国大会
    • Place of Presentation
      富山国際会議場
    • Related Report
      2013 Annual Research Report
  • [Presentation] 拡張融合法に基づく次世代SATソルバーの試作2013

    • Author(s)
      森 淳,鍋島 英知
    • Organizer
      第27回人工知能学会全国大会
    • Place of Presentation
      富山国際会議場
    • Related Report
      2013 Annual Research Report
  • [Presentation] 高速SATソルバーの実装と理論2013

    • Author(s)
      鍋島英知
    • Organizer
      第15回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      東山温泉御宿東鳳(福島県会津若松市)
    • Related Report
      2012 Research-status Report
    • Invited
  • [Presentation] A Best-First Search Strategy for SOL Tableau Calculus2012

    • Author(s)
      H. Nabeshima
    • Organizer
      The 4th JFLI-LRI-NII Workshop on Consequence Finding and Satisfiability Testing in Distributed Environments and Systems Biology
    • Place of Presentation
      LRI(フランス)
    • Year and Date
      2012-11-19
    • Related Report
      2013 Final Research Report
  • [Presentation] 結論発見システム SOLAR の分割統治法による高速化2012

    • Author(s)
      寄特 勇紀,鍋島 英知
    • Organizer
      第26回人工知能学会全国大会
    • Place of Presentation
      山口県教育会館(山口県)
    • Year and Date
      2012-06-12
    • Related Report
      2013 Final Research Report
  • [Presentation] 高速充足可能性判定器を用いた命題論理の結論発見器の実装2012

    • Author(s)
      村松 匠,鈴木 健士郎,鍋島 英知,岩沼 宏治
    • Organizer
      第26回人工知能学会全国大会
    • Place of Presentation
      山口県教育会館(山口県)
    • Year and Date
      2012-06-12
    • Related Report
      2013 Final Research Report
  • [Presentation] 学習節評価尺度LBD に基づく並列SAT ソルバーの提案2012

    • Author(s)
      大橋 弘幸,鍋島 英知
    • Organizer
      第26回人工知能学会全国大会
    • Place of Presentation
      山口県教育会館(山口県)
    • Year and Date
      2012-06-12
    • Related Report
      2013 Final Research Report
  • [Presentation] 高速SAT ソルバーの実装と理論2012

    • Author(s)
      鍋島 英知
    • Organizer
      第15回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      御宿東鳳(福島県)
    • Year and Date
      2012-03-05
    • Related Report
      2013 Final Research Report
    • Invited
  • [Presentation] 充足可能性判定器に基づく命題論理の結論発見器の提案2012

    • Author(s)
      鈴木 健士郎,鍋島 英知,岩沼 宏治
    • Organizer
      第85回人工知能学会人工知能基本問題研究会
    • Place of Presentation
      KKR 下呂しらさぎ(岐阜県)
    • Year and Date
      2012-02-03
    • Related Report
      2013 Final Research Report
  • [Presentation] SAT ソルバーの探索戦略効率化に向けた合理的尺度の導入検証2012

    • Author(s)
      村松 匠,鍋島 英知
    • Organizer
      第85回人工知能学会人工知能基本問題研究会
    • Place of Presentation
      KKR 下呂しらさぎ(岐阜県)
    • Year and Date
      2012-02-03
    • Related Report
      2013 Final Research Report
  • [Presentation] SOL タブロー計算法の分割統治アルゴリズムの検討2012

    • Author(s)
      寄特 勇紀,鍋島 英知
    • Organizer
      第85回人工知能学会人工知能基本問題研究会
    • Place of Presentation
      KKR 下呂しらさぎ(岐阜県)
    • Year and Date
      2012-02-03
    • Related Report
      2013 Final Research Report
  • [Presentation] 結論発見システム SOLAR の分割統治法による高速化2012

    • Author(s)
      寄特勇紀,鍋島英知
    • Organizer
      第26回人工知能学会全国大会
    • Place of Presentation
      山口県教育会館(山口県山口市)
    • Related Report
      2012 Research-status Report
  • [Presentation] 高速充足可能性判定器を用いた命題論理の結論発見器の実装2012

    • Author(s)
      村松匠,鈴木健士郎,鍋島英知,岩沼宏治
    • Organizer
      第26回人工知能学会全国大会
    • Place of Presentation
      山口県教育会館(山口県山口市)
    • Related Report
      2012 Research-status Report
  • [Presentation] 学習節評価尺度LBDに基づく並列SATソルバーの提案2012

    • Author(s)
      大橋弘幸,鍋島英知
    • Organizer
      第26回人工知能学会全国大会
    • Place of Presentation
      山口県教育会館(山口県山口市)
    • Related Report
      2012 Research-status Report
  • [Presentation] 充足可能性判定器に基づく命題論理の結論発見器の提案2012

    • Author(s)
      鈴木 健士郎,鍋島 英知,岩沼 宏治
    • Organizer
      第85回人工知能学会人工知能基本問題研究会
    • Place of Presentation
      下呂交流会館(岐阜県)
    • Related Report
      2011 Research-status Report
  • [Presentation] SATソルバーの探索戦略効率化に向けた合理的尺度の導入検証2012

    • Author(s)
      村松 匠,鍋島 英知
    • Organizer
      第85回人工知能学会人工知能基本問題研究会
    • Place of Presentation
      下呂交流会館(岐阜県)
    • Related Report
      2011 Research-status Report
  • [Presentation] SOLタブロー計算法の分割統治アルゴリズムの検討2012

    • Author(s)
      寄特 勇紀,鍋島 英知
    • Organizer
      第85回人工知能学会人工知能基本問題研究会
    • Place of Presentation
      下呂交流会館(岐阜県)
    • Related Report
      2011 Research-status Report
  • [Presentation] 局所対称性除去による CDCL ソルバーの効率改善に向けて2011

    • Author(s)
      金澤 潤二,鍋島 英知
    • Organizer
      第84回人工知能学会人工知能基本問題研究会
    • Place of Presentation
      慶応義塾大学
    • Year and Date
      2011-12-16
    • Related Report
      2013 Final Research Report
  • [Presentation] Scalability Improvement of SOL Tableau Calculus based on a Divide-and-Conquer Strategy2011

    • Author(s)
      H. Nabeshima, K. Iwanuma, K. Inoue
    • Organizer
      The 3rd LRI-NII Collaborative Meeting on Distributed Reasoning and Problem Decomposition
    • Place of Presentation
      LRI(フランス)
    • Year and Date
      2011-10-31
    • Related Report
      2013 Final Research Report
  • [Presentation] 局所対称性除去によるCDCL ソルバーの効率化手法の検討2011

    • Author(s)
      金澤 潤二,鍋島 英知
    • Organizer
      日本ソフトウェア科学会第28回大会
    • Place of Presentation
      沖縄産業支援センター(沖縄県)
    • Year and Date
      2011-09-27
    • Related Report
      2013 Final Research Report
  • [Presentation] SOL タブロー計算法に基づく命題論理の充足可能性判定器の実現2011

    • Author(s)
      鈴木 健士郎, 鍋島 英知
    • Organizer
      第25回人工知能学会全国大会
    • Place of Presentation
      いわて県民情報交流センター(岩手県)
    • Year and Date
      2011-06-03
    • Related Report
      2013 Final Research Report
  • [Presentation] ポートフォリオ型戦略の導入による結論発見システムSOLAR の効率改善2011

    • Author(s)
      村松 匠, 鍋島 英知
    • Place of Presentation
      いわて県民情報交流センター(岩手県)
    • Year and Date
      2011-06-02
    • Related Report
      2013 Final Research Report
  • [Presentation] 結論発見手続きSOL タブロー計算法の分割統治法に基づく効率化2011

    • Author(s)
      寄特 勇紀, 鍋島 英知
    • Organizer
      第25回人工知能学会全国大会
    • Place of Presentation
      いわて県民情報交流センター(岩手県)
    • Year and Date
      2011-06-01
    • Related Report
      2013 Final Research Report
  • [Presentation] 局所対称性除去による CDCL ソルバーの効率改善に向けて2011

    • Author(s)
      金澤 潤二,鍋島 英知
    • Organizer
      第84回人工知能学会人工知能基本問題研究会
    • Place of Presentation
      慶応義塾大学 日吉キャンパス(神奈川県)
    • Related Report
      2011 Research-status Report
  • [Presentation] GlueMiniSat 2.2.5:単位伝播を促す学習節の積極的獲得戦略に基づく高速SAT ソルバー2011

    • Author(s)
      鍋島 英知,岩沼 宏治,井上 克巳
    • Organizer
      日本ソフトウェア科学会第28回大会
    • Place of Presentation
      沖縄産業支援センター(沖縄県)
    • Related Report
      2011 Research-status Report
  • [Presentation] 局所対称性除去によるCDCLソルバーの効率化手法の検討2011

    • Author(s)
      金澤 潤二,鍋島 英知
    • Organizer
      日本ソフトウェア科学会第28回大会
    • Place of Presentation
      沖縄産業支援センター(沖縄県)
    • Related Report
      2011 Research-status Report
  • [Presentation] SOL タブロー計算法に基づく命題論理の充足可能性判定器の実現2011

    • Author(s)
      鈴木 健士郎, 鍋島 英知
    • Organizer
      第25回人工知能学会全国大会
    • Place of Presentation
      アイーナ いわて県民情報交流センター(岩手県)
    • Related Report
      2011 Research-status Report
  • [Presentation] 結論発見手続き SOL タブロー計算法の分割統治法に基づく効率化2011

    • Author(s)
      寄特 勇紀, 鍋島 英知
    • Organizer
      第25回人工知能学会全国大会
    • Place of Presentation
      アイーナ いわて県民情報交流センター(岩手県)
    • Related Report
      2011 Research-status Report
  • [Presentation] ポートフォリオ型戦略の導入による結論発見システム SOLAR の効率改善2011

    • Author(s)
      村松 匠, 鍋島 英知
    • Organizer
      第25回人工知能学会全国大会
    • Place of Presentation
      アイーナ いわて県民情報交流センター(岩手県)
    • Related Report
      2011 Research-status Report
  • [Presentation] 一般双対化問題における 冗長節生成の抑制法とその評価2011

    • Author(s)
      山本 泰生,鍋島 英知,岩沼 宏治
    • Organizer
      第25回人工知能学会全国大会
    • Place of Presentation
      アイーナ いわて県民情報交流センター(岩手県)
    • Related Report
      2011 Research-status Report
  • [Remarks] 結論発見システム SOLAR

    • URL

      http://solar.nabelab.org/

    • Related Report
      2013 Final Research Report
  • [Remarks] 命題論理の充足可能性判定器 GlueMiniSat

    • URL

      http://glueminisat.nabelab.org/

    • Related Report
      2013 Final Research Report
  • [Remarks] 結論発見システム SOLAR

    • URL

      http://solar.nabelab.org/

    • Related Report
      2013 Annual Research Report
  • [Remarks] 命題論理の充足可能性判定器 GlueMiniSat

    • URL

      http://glueminisat.nabelab.org/

    • Related Report
      2013 Annual Research Report
  • [Remarks] 結論発見システム SOLAR

    • URL

      http://solar.nabelab.org/

    • Related Report
      2012 Research-status Report
  • [Remarks] 命題論理の充足可能性判定器 GlueMiniSat

    • URL

      http://glueminisat.nabelab.org/

    • Related Report
      2012 Research-status Report
  • [Remarks]

    • URL

      http://solar.nabelab.org/

    • Related Report
      2011 Research-status Report
  • [Remarks]

    • URL

      http://glueminisat.nabelab.org/

    • Related Report
      2011 Research-status Report

URL: 

Published: 2011-08-05   Modified: 2019-07-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi