著者

迫 龍哉 宋 剛秀 番原 睦則 田村 直之 鍋島 英知 井上 克巳

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.33, no.4, pp.4_16-4_29, 2016-10-25 (Released:2017-01-14)

---

近年,命題論理の充足可能性判定(SAT)問題を解くSATソルバーの飛躍的な性能向上を背景に,問題をSATに変換し,SATソルバーを用いて求解するSAT型ソルバーが成功を収めている.しかしながら,最適化問題,解列挙問題などに対しては,SATソルバーを複数回起動する必要があり,求解性能が大きく低下することがある.この問題を解決する方法として,インクリメンタルSAT解法の利用が挙げられる.SATソルバー競技会のひとつであるSAT Race 2015で,このような解法を容易に実現するためのインクリメンタルSAT APIが提案された.本論文では,それを拡張したインクリメンタルSAT APIであるiSATを提案し,その応用について述べる.提案する拡張により,問題を簡潔に記述でき,Javaからの利用も可能になる.また,ショップスケジューリング問題,N-クイーン問題,ハミルトン閉路問題に対する実験結果を通じ,iSAT利用の有効性を示す.

著者

井上 克巳 坂間 千秋

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.25, no.3, pp.3_20-3_32, 2008-07-25 (Released:2008-09-30)

被引用文献数

1

---

Prologがベースとしているホーン節論理に基づく論理プログラミングでは,構文的制約があって確定的知識しか表現できないことが,現実的な知識表現のためには限界であるとされていた.この問題点を克服するために,論理プログラミングにおいて不完全・不確定な情報を扱うための拡張理論が1980年代後半から数多く提案された.1999年にはこれらに加えて制約プログラミングの概念を融合した解集合プログラミングの概念が確立され,現在では論理プログラミングの中心的な研究テーマの1つになっている.本稿では過去からのこうした研究の流れと新しい論理プログラミングの可能性について探る.

著者

井上 克巳 田村 直之 Katsumi Inoue Naoyuki Tamura

出版者

人工知能学会

雑誌

人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence (ISSN:09128085)

巻号頁・発行日

vol.25, no.1, pp.57-67, 2010-01-01

参考文献数

56

被引用文献数

8

著者

新田 克己 柴崎 真人 安村 禎明 長谷川 隆三 藤田 博 越村 三幸 井上 克巳 白井 康之 小松 弘

出版者

一般社団法人 人工知能学会

雑誌

人工知能学会論文誌 (ISSN:13460714)

巻号頁・発行日

vol.17, no.1, pp.32-43, 2002 (Released:2002-04-04)

参考文献数

23

---

We present an overview of a legal negotiation support system, ANS (Argumentation based Negotiation support System). ANS consists of a user interface, three inference engines, a database of old cases, and two decision support modules. The ANS users negotiates or disputes with others via a computer network. The negotiation status is managed in the form of the negotiation diagram. The negotiation diagram is an extension of Toulmin’s argument diagram, and it contains all arguments insisted by participants. The negotiation protocols are defined as operations to the negotiation diagram. By exchanging counter arguments each other, the negotiation diagram grows up. Nonmonotonic reasoning using rule priorities are applied to the negotiation diagram.

著者

番原 睦則 田村 直之 井上 克巳

出版者

一般社団法人日本ソフトウェア科学会

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.24, no.3, pp.75-86, 2007-07-26

被引用文献数

1

---

本論文では,PrologからJavaへのトランスレータ処理系Prolog Cafeについて述べる.本システムでは,Prologプログラムは,WAMを介して,Javaプログラムに変換され,既存のJava処理系を用いてコンパイル・実行される.つまりProlog Cafeでは,項,述語などPrologの構成要素のすべてがJavaに変換される.このため,PrologCafeはJavaとの連携,拡張性に優れたProlog処理系となっている.Prolog Cafeはマルチスレッドによる並列実行をサポートしており,スレッド間の通信は共有Javaオブジェクトにより実現される.また任意のJavaオブジェクトをPrologの項として取り扱う機能を有しており,Prologからメソッド呼び出し,フィールドへのアクセスも行える.最後にProlog Cafeの応用として,複数SATソルバの並列実行システムMultisatについて述べる.

著者

井上 克巳

出版者

一般社団法人 人工知能学会

雑誌

人工知能 (ISSN:21882266)

巻号頁・発行日

vol.25, no.3, pp.389-399, 2010-05-01 (Released:2020-09-29)

著者

井上 克巳

出版者

一般社団法人 人工知能学会

雑誌

人工知能 (ISSN:21882266)

巻号頁・発行日

vol.7, no.1, pp.48-59, 1992-01-01 (Released:2020-09-29)

著者

井上 克巳

雑誌

情報処理

巻号頁・発行日

vol.57, no.8, pp.720-723, 2016-07-15

---

SATは計算機科学において最も単純で基本的な問題であるとともに,人工知能(AI)においても推論や制約充足のベースとなる重要な問題である.またSAT技術もアルゴリズム分野というよりは,AI研究の中で発展してきたことは注目に値する.本稿では,SATとAIの密接な関係を歴史的に概観し,SATがどれだけAIにインパクトを与えてきて,今後のAI 技術を左右し得るかについて予測する.SATは問題の構造が単純過ぎて(また理論的にもクラスNP に属するため)AIの本質的な複雑さには到底及ばないという意見があるにもかかわらず,SATの深遠さを知ることがAIに通ずることを本稿から読み取っていただきたい.

著者

沖本 天太 生貝 直人 リベイロ トニー 井上 克巳 岡田 仁志 丸山 宏

出版者

FIT(電子情報通信学会・情報処理学会)運営委員会

雑誌

情報科学技術フォーラム講演論文集

巻号頁・発行日

vol.12, no.4, pp.477-484, 2013-08-20

著者

鍋島 英知 岩沼 宏治 井上 克巳

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.29, no.4, pp.4_146-4_160, 2012-10-25 (Released:2012-11-25)

---

命題論理の充足可能性判定問題(SAT問題)を解くソルバーは,その飛躍的な性能向上に伴い,システム検証やプランニング・スケジューリング問題,制約充足・最適化問題等の様々な分野において活躍している.GlueMiniSat 2.2.5は,単位伝搬を促し矛盾の発生を促進する学習節を積極的に獲得する戦略に基づくSATソルバーである.学習節の評価尺度には,AudemardとSimonが開発したSATソルバーGlucoseで導入されたリテラルブロック距離を改良した尺度を用い,単位伝搬を促進する学習節を獲得・保持する.また良い学習節の獲得を促すため,非常に積極的なリスタート戦略を採る.我々は代表的SATソルバーであるMiniSat 2.2を基にこれらの手法を実装し,GlueMiniSat 2.2.5を開発した.GlueMiniSat 2.2.5は充足不能性の証明に強く,SAT 2011競技会のApplication部門において逐次型ソルバーとしてUNSATクラスで1位,SAT+UNSATクラスで2位を獲得している.また並列型ソルバーを含めても同部門UNSATクラスで2位を獲得している.

著者

寸田 智也 宋 剛秀 番原 睦則 田村 直之 井上 克巳

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.59, no.9, pp.1749-1760, 2018-09-15

---

本論文では,トークン数が整数値である一般のペトリネットを対象とし,そのデッドロック検出についてSAT技術を用いた手法を提案する.提案手法では,非負整数値であるトークン数を表現するために順序符号化を採用することで,既存のSAT型手法では対応できなかった一般のペトリネットでのデッドロック検出を実現した.また,既存SAT型手法で採用されていたモデル(連続発火モデルと呼ぶ)よりも短いステップ長でデッドロック検出が可能となる多重発火モデルを提案し,性能向上を実現した.評価実験では,Model Checking Contest 2017のベンチマーク問題を用いて,連続発火モデルと多重発火モデルを比較した.ほぼすべての問題で多重発火モデルのほうが優れていたが,特に初期マーキングのトークン数が比較的多い問題に対する効果が大きかった.また,Model Checking Contest 2017デッドロック検出部門での優勝ソルバLoLAおよび準優勝ソルバTapaalとの比較を行った.提案手法は,デッドロックを検出できた問題数ではLoLA,Tapaalより少なかったが,LoLAおよびTapaalを含めたすべてのソルバがデッドロック検出に失敗した問題での検出に成功し,提案手法の有効性が確認できた.In this paper, we propose a SAT-based method to detect deadlock of general Petri nets in which more than one tokens are allowed for each place. In our approach, the transition relation of a Petri net is represented as constraints on integers and they are translated into SAT by order encoding, so that the deadlock of general Petri nets can be detected by a SAT solver, while existing SAT-based methods cannot be applied for them. Furthermore, in order to improve the performance, we introduced multiple firing model, which can detect deadlock with shorter steps than the model used in an existing SAT-based method, called successive firing model. We evaluated the successive firing model and the multiple firing model through a benchmark set of Model Checking Contest 2017. The multiple firing model showed better performance for almost all instances, and was especially effective for the instances in which there are many tokens at the initial marking. Through the comparison with the winner tool LoLA and the second place tool Tapaal of the contest, although the number of detected deadlocks are fewer than LoLA and Tapaal, we confirmed the effectiveness of the proposed method with some instances for which all tools including LoLA and Tapaal failed to detect deadlock.

著者

井上 克巳 Katsumi Inoue

雑誌

人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence (ISSN:09128085)

巻号頁・発行日

vol.7, no.1, pp.48-59, 1992-01-01

著者

岡崎 孝太郎 井上 克巳

出版者

人工知能学会

雑誌

人工知能学会全国大会論文集 (ISSN:13479881)

巻号頁・発行日

vol.31, 2017

---

テレビ放送の世帯視聴はスマートフォン経由の個人視聴へ劇的に移行し,一斉かつ受動的な視聴からの解放が進む.本論文は,SNSを介した内生的ネットワークが創発する視聴拡散パターンを捉える技術フレームワークを呈示する.シングルソースの変換した媒体クラスを跨ぐ視聴履歴から,潜在視聴の状態空間モデルと視聴態度間の因果グラフを抽出する.人工知能技術がテレビビジネスの新しい展開へ貢献する野心的な取り組みである.

著者

沖本 天太 井上 克巳

出版者

神戸大学

雑誌

基盤研究(C)

巻号頁・発行日

2014-04-01

---

本研究では動的環境における多目的分散制約最適化に関する研究を行った.まず,多目的分散制約最適化アルゴリズムとして,すべてのパレート最適解が求解可能な厳密アルゴリズム,パレートフロントの部分集合を求解する非厳密アルゴリズム,パレートフロントの近似解を求解する近似アルゴリズムをそれぞれ開発した.次に,動的環境における多目的分散制約最適化問題を定式化し,この問題を解く効率的なアルゴリズムを提案した.最後に,応用研究として,チーム編成問題及びナース・スケジューリング問題に本モデルを適用した.本研究は,申請書に記載した研究計画どおりに進めることが出来,AI分野の最難関国際会議に複数の論文を輩出している.

著者

井上 克巳 坂間 千秋

出版者

国立情報学研究所

雑誌

挑戦的萌芽研究

巻号頁・発行日

2014-04-01

---

時間的に変化する離散系を標準論理プログラムで記述し、その上での帰納推論方式を新たに考案し、状態遷移規則を学習するための方法論を提案する。基本方式として状態間の変位からブーリアンネットワークの状態遷移規則を自動的に学習するLFITを提案し、これをベースに様々な効率化や拡張方式を開発した。効率化にはBDDによる簡約化やトップダウン・アルゴリズムが、拡張には遅延効果・多値ドメイン・確率遷移を有するネットワークと非同期式更新が含まれる。LFITの応用では、遺伝子制御ネットワークやセルオートマトン学習、ロボットの行動規則学習、論理を自動的に学習する論理発見に適用した。

著者

井上 克巳

出版者

社団法人人工知能学会

雑誌

人工知能学会誌 (ISSN:09128085)

巻号頁・発行日

vol.25, no.3, pp.389-399, 2010-05-01

被引用文献数

2

著者

佐藤 健 井上 克巳 岩沼 宏治 坂間 千秋

出版者

一般社団法人日本ソフトウェア科学会

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.20, no.1, pp.27-35, 2003-01-24

被引用文献数

1

---

現在のマルチエージェントシステムでは,エージェントが他エージェントに質問を与えた場合に, 質問を受けたエージェントが答を返すまでは, 質問したエージェントの処理は中断されることが普通である. インターネットのような通信が必ずしも保証されていないような環境下においては, このような中断がデッドロックを引き起こすことがありうる.また, たとえ通信が完全であっても, 他エージェントの処理に時間がかかっていれば、通信が不完全な状態と同じような状態になることがありうる. 本論文は、このような通信が必ずしも保証されていないマルチエージェントシステムにおける分散問題解決の手法を与える. 本手法は, 質問に対するデフォルトの回答を用意しておき, 回答が戻らなくても, デフォルトを用いて計算を進め, その後, 送られてきた真の回答がデフォルトと異なるときのみ, 計算をやり直すというものである. 本論文では, マスタースレーブマルチエージェントシステムにおいて,副作用が存在しない処理での投機的計算手法を仮説論理プログラミングの枠組みで実現し, 手法の健全性を示す.

著者

井上 克巳 坂間 千秋

出版者

一般社団法人日本ソフトウェア科学会

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.25, no.3, pp.20-32, 2008-07-25

被引用文献数

7

---

Prologがベースとしているホーン節論理に基づく論理プログラミングでは,構文的制約があって確定的知識しか表現できないことが,現実的な知識表現のためには限界であるとされていた.この問題点を克服するために,論理プログラミングにおいて不完全・不確定な情報を扱うための拡張理論が1980年代後半から数多く提案された. 1999年にはこれらに加えて制約プログラミングの概念を融合した解集合プログラミングの概念が確立され,現在では論理プログラミングの中心的な研究テーマの1つになっている.本稿では過去からのこうした研究の流れと新しい論理プログラミングの可能性について探る.