分散並列型SATソルバにおける探索空間の分割手法の提案
スポンサーリンク
概要
- 論文の詳細を見る
命題論理の充足可能性問題(satisfiability problem;SAT問題)は計算機科学や人工知能の基礎となる最重要問題の一つであり,プランニングやスケジューリング,有界モデル検査,暗号の検証など多くの実用的応用を持つ.このSAT問題を解くSATソルバは,近年劇的な性能向上を果たしており,様々な分野で利用され始めている.本研究では高速な分散並列型SATソルバの開発を目的としており,(1)網羅的な問題分割,(2)網羅的な問題分割と多重探索戦略の併用,(3)ランダムな問題分割の3種類の実装を行った.またソルバ間で各ソルバが探索の過程で生成した学習節の共有も行っている.実験の結果,3つの手法で共に線形効果が得られ,(2)は(1)よりも高速に解けていることから多重探索戦略が効果的であることを示しており,(3)は充足可能な問題に対して高い性能を示していることを確認した.
- 2009-02-23
著者
-
岩沼 宏治
山梨大学大学院医学工学総合研究部
-
鍋島 英知
山梨大学大学院医学工学総合研究部
-
高見 明秀
山梨大学大学院医学工学総合教育部コンピュータ・メディア工学専攻
-
岩沼 宏治
山梨大学大学院コンピュータメディア工学専攻
-
岩沼 宏治
山梨大学大学院工学総合研究部
-
岩沼 宏治
山梨大学大学院 医学工学総合研究部
関連論文
- SATによるプランニングとスケジューリング(最近のSAT技術の発展)
- SMT:個別理論を取り扱うSAT技術(最近のSAT技術の発展)
- 高速SATソルバーの原理(最近のSAT技術の発展)
- SMT : 個別理論を取り扱うSAT技術
- WEB検索高度化のためのアンサンブル学習に基づく訓練事例の精錬 (人工知能と知識処理)
- 情報利得基準に基づく系列データマイニングによるイベント系列コーパス作成実験 (特集 「知見の創出を目指した情報技術」および一般)
- マルチモーダルユーザインターフェースを備えた高次コミュニケーション空間の構築に関する研究開発通信放送機構委託研究(1997-2001)
- 分散並列型SATソルバにおける探索空間の分割手法の提案
- 検索隠し味の半自動生成を目的とした訓練データの精製(「自動推論: 帰納, 演繹, モデル検査/生成, 学習, 発見, 仮説推論, 論理プログラミング, プランニングetc.」及び一般)
- 系列パターンマイニングにおけるアイテム集合間の関連強度による頻出部分系列の絞込み(「自動推論: 帰納, 演繹, モデル検査/生成, 学習, 発見, 仮説推論, 論理プログラミング, プランニングetc.」及び一般)
- SOLにおけるタブ口証明反転法とその応用(「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論、論理プログラム,プランニングetc.」及び一般)
- 補題再利用によるSATプランニングの高速化(「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(自動推論)
- 投機的計算によるSATプランニングの効率改善に関する研究(自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
- 効率的なSATプランニングとSATスケジューリングのための補題再利用(「自動化:推論,発見,学習,データマイニング」及び一般)
- WEB検索高度化のためのアンサンブル学習に基づく訓練事例の精錬(「Webインテリジェンス」及び一般)
- Webアクセスログに対する系列データマイニング : ページ滞在時間系列の解析(「さまざまな分野の形式的検証最前線」及びAI一般)
- 因果関係抽出を目的としたコンフィデンスに基づく高速系列データマイニング (「生命情報からの知識発見」及び一般)
- 極大系列抽出を目的とする系列包含検査の高速化アルゴリズム(「さまざまな分野の形式的検証最前線」及びAI一般)
- 山梨大学学内情報基盤(YINS)の概要 (第10回学術情報処理研究集会)
- リテラルブロック距離に基づく良い学習節の評価と獲得によるSATソルバの性能改善 (特集 「AIの基本問題SATと応用技術」および一般)
- Non-monotone dualization via monotone dualization (特集 「AIの基本問題SATと応用技術」および一般)
- LF-012 単一の長大なデータ系列上の系列パターンの出現尺度とその逆単調性(F. 人工知能)
- 一般講演 単一の長大なテキストデータ系列からの頻出パターンの発見 (ことば工学研究会(第17回)テーマ:物語とコミュニケーション:その性質と生成)
- Semantic Model Elimination : Toward Efficient Equality Proving : Extended Abstract
- マルチ移動エージェントシステムにおける記憶情報のピアツーピア通信に基づく大域的最適化
- LL_005 専門検索エンジンの高速半自動生成法(L分野:ネットワークコンピューティング)
- 専門検索エンジンの半自動生成を目的とした類似度に基づくWEB学習データの精製(一般,コミュニケーションとAI及び一般)
- L-083 精錬手法に基づく検索隠し味型専門検索エンジンの半自動構築(L分野:ネットワークコンピューティング)
- 情報量と頻度に基づく非同期かつ有用な系列パターンの高速抽出
- F-043 精度保証付きオンライン型高速近似系列マイニング(人工知能・ゲーム,一般論文)
- 時間的差分データの監視を目的とした携帯端末画面への表示システムに関する研究
- 時間的差分データの監視を目的とした携帯端末画面への表示システムに関する研究
- HTML文書の時間的差分の自動検出に関する研究 (テーマ:一般演題及び「webとtext」)
- エージェント間通信におけるアブダクションによる投機的計算(マルチエージェント)
- 特集「定理証明, 推論関係の新技術」にあたって
- F-045 マルチコア環境に向けた高速並列SATソルバの開発(F分野:人工知能・ゲーム)
- マルチコア環境に向け並列SATソルバの開発(「自動化:推論,発見,学習,データマイニング」及び一般)
- 文法推論に基づく無損失データ圧縮の改善(一般セッション,LDPC符号,及び一般)
- F-019 文法推論に基づく無損失データ圧縮の改善(人工知能・ゲーム,一般論文)
- HTMLからXMLへの事例ベース変換における複合テキストブロックの取扱い : アライメント等の適用
- 事例に基づくHTML文書からXML文書への半自動変換 : シリーズ型HTML文書における類似性の利用
- タブローに基づく論理的帰結発見手続きSOL
- F-047 イベント時系列マイニングを目的とする新聞記事からの時系列情報に基づく単語抽出(人工知能・ゲーム,一般論文)
- イベント系列マイニングを目的とする新聞記事からの時系列情報に基づく単語抽出 (「生命情報からの知識発見」及び一般)
- SATソルバと後ろ向き推論によるアクション言語Αの実装
- アクション言語のためのボトムアップ処理系
- 階層パターンの抽出を目指した系列データマイニング(学生セッション,大学のAI・企業のAI)
- 階層パターンの抽出を目指した系列データマイニング(学生セッション,大学のAI・企業のAI)
- 結論発見手続きSOLタブロー法のための多重探索戦略の提案 (特集 「ベイジアン・ネットワーク」および一般)
- F-021 情報量と頻度に基づく系列データマイニングにおける非同期パターンの抽出と効率化(人工知能・ゲーム,一般論文)
- Nelson-Oppen結合手続きの逆伴意法に基づく改良
- エージェントのルール学習におけるGAとGPの特性比較と融合化による性能向上
- エージェントの行動学習問題におけるGAとGPの特性解析とハイブリッド化による性能向上
- エージェントの行動学習におけるGAとGPの性能比較
- 専門語彙テンプレートの自動生成とWebページの自動統合(WWW,テキスト情報の要約と掲示に関わる自然言語処理シンポジウム及び一般)
- アクション言語Aにおける行動規則の学習
- 非決定性アクション言語NA上のプランニング手続き
- SATソルバによるアクション言語処理系の実装
- SATソルバによるアクション言語処理系の実装
- 有限オートマトンに基づく非決定性アクション言語
- 事例に基づくシリーズ型HTML文書の意味論理構造の自動認識 : HTMLからXMLへの自動変換を目指して
- シリーズ型HTML文書の事例に基づく文書論理構造の自動認識と抽出 (テーマ:一般演題及び「webとtext」)
- アクション言語Aにおける行動規則の学習
- WEB文書の頻出語情報を利用した解答検索システムの構築(一般,コミュニケーションとAI及び一般)
- 近年の一階論理定理証明プログラムの実際
- 共通記号を持つ背景理論の決定手続きの結合法とその効率化について
- LF_006 緩和法に基づく系列データからの頻出部分系列の高速マイニング(F分野:人工知能・ゲーム)
- 背景記事集合の類似度に基づく新聞記事のクラスタリング(一般,テキスト情報の要約と掲示に関わる自然言語処理シンポジウム及び一般)
- 緩和法に基づく時系列データ中からの頻出部分系列の高速マイニング (テーマ:「データマイニングと統計数理」および一般)
- 時系列データ中の頻出部分系列を高速抽出するオンライン近似計算法 (テーマ:「データマイニングと統計数理」および一般)
- 論理プログラムによるゲームのプロトタイプ開発支援ツールGALOPの開発
- LF-002 大規模データ系列中に頻出する部分系列のオンライン抽出アルゴリズム(F分野:人工知能・ゲーム)
- リンク元コンテキストを用いたWEB文書の最重要箇所の同定法
- マルチエージェントシステム分散協調問題における時間遅れと知識量の関係
- 利己的なマルチエージェント群の分散協調における時間遅れの影響
- アクション言語Αのためのオートマトン理論
- プランニンググラフとSATプランニング(「プランニング技術の進展と新たな応用展開」)
- ハイパーリンク先ページでの重要箇所の同定法:リンク元コンテキストとページ構造の考慮 (特集 「医療及び化学情報マイニング」および一般)
- 老若男女だれでも簡単に使えるHTML文書ラッパ自動合成システム(「21世紀の知識情報科学に向けて」,及び一般)
- リンク元コンテキストを考慮するハイパーリンク重要箇所同定法
- 近年の定理自動証明技術 : システムコンペCASCとその周辺(「定理証明, 推論関係の新技術」)
- Java言語によるアクション言語処理系の実装
- アクション言語Aにおける因果関係の学習
- アクション言語における非決定性アクションの表現と推論に関する考察
- アクション言語Aを表現するオートマトンモデル
- 多値論理を用いた生体ネットワークシステムのモデル検査(2012年5月28日版)
- テキスト系列マイニングにおける有用性尺度について(系列パターンマイニングの最近の動向)
- 充足可能性判定器に基づく命題論理の結論発見器の提案 (「マルチエージェントの基礎理論とその応用」および一般)
- 系列パターン抽出における各種の評価尺度の関係性 (「マルチエージェントの基礎理論とその応用」および一般)
- 多値論理を用いた生体ネットワークシステムのモデル検査(2012年5月28日版) (ニューロコンピューティング)
- 多値論理を用いた生体ネットワークシステムのモデル検査 : 2012年5月28日版(一般,機械学習によるバイオデータマインニング,一般)