論理式の充足可能性問題における変数の依存関係に基づく効率的な変数決定順序(HPC-5: 数値計算アルゴリズム(2))
スポンサーリンク
概要
- 論文の詳細を見る
論理式の充足可能性問題(SAT問題)を解くには, 論理式の中の変数をある順番で選んで真理値を代入して充足されなければ別の組み合わせを選び, 可能なすべての場合をチェックするアルゴリズムが広く用いられている.このようなアルゴリズムでは, どのような順序で変数値を決定するかが効率を大きく左右する.我々の提案する変数の順序づけの方法は, 変数間の依存関係を計算し, 他の変数に依存する変数よりも, 他の変数に依存しない独立な変数の値をより早く決定する.この方法は, SAT問題の応用分野のひとつであるモデル検証における, 状態遷移モデルの構造的な性質を捉えており, 8ビットの乗算回路を用いた実験では, 高速なSAT solverであるzChaffを200倍近く高速化することができた.
- 一般社団法人情報処理学会の論文
- 2005-08-03
著者
-
鴨志田 良和
東京大学
-
田浦 健次朗
東京大学大学院情報理工学系研究科
-
田浦 健次朗
東大 大学院情報理工学系研究科
-
田浦 健次朗
東京大学
-
近山 隆
東京大学大学院 新領域創成科学研究科 基盤情報学専攻
-
近山 隆
東京大学大学院工学系研究科
-
近山 隆
東京大学
-
近山 隆
日本ソフトウェア技術会
-
近山 隆
東大
-
近山 隆
新世代コンピュータ技術開発機構
-
鴨志田 良和
東京大学情報基盤センター
関連論文
- メッセージ衝突を防止する適応的な収集操作アルゴリズム(並列分散処理,情報爆発論文)
- 並列分散環境におけるファイル共有システムの負荷原因探索システム(ストレージアクセス技術,2009年並列/分散/協調処理に関する『仙台』サマー・ワークショップ(SWoPP仙台2009))
- ファイルステージング再考 : オンデマンド化と高速化に向けたプロトタイプ実装の評価(ファイルシステム,「ハイパフォーマンスコンピューティングとアーキテクチャの評価」に関する北海道ワークショップ(HOKKE-2009))
- 並列プログラムの実行可搬性を実現するMPI通信ライブラリの設計(インターコネクト/MPI通信ライブラリ,「ハイパフォーマンスコンピューティングとアーキテクチャの評価」に関する北海道ワークショップ(HOKKE-2009))
- 大規模クラスタを用いた高精度なGait認識(一般セッション(2),文字認識・文書理解)
- 大規模クラスタを用いた高精度なGait認識(一般セッション(2), 文字認識・文書理解)
- 複数拠点に分散配置されたクラスタの効率的な管理手法(セッション6:分散システム)
- GAとTD(λ)学習の組み合わせによるゲーム局面評価パラメータの調整(学習1)
- グリッド用シェルGXPの長時間計算のための拡張(HPC-17 : グリッド)
- 対訳辞書のグラフ表現を用いた日英対訳テキストの発見(文書処理,質問応答)
- CHLAC特徴とGridコンピューティングを併用したリアルタイム動作認識(一般セッション(2),文字認識・文書理解)
- CHLAC特徴とGridコンピューティングを併用したリアルタイム動作認識(一般セッション(2), 文字認識・文書理解)
- 5K-2 実世界情報並列計算基盤の開発(情報爆発時代における分散システム技術,一般セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 並列処理のための効率的なトポロジ推定(HPC-10 : 適応環境での通信)
- 3.Javaにおける並列プログラミングサポート(マルチコアを活かすお手軽並列プログラミング)
- グリッドチャレンジテストベッドの構築と運用 : グリチャレテストベッドの作り方(HPC-3 : 大規模運用システム(1))
- 情報爆発時代における安全・安心ITシステム基盤(情報爆発時代に向けた新しいIT基盤技術の研究)
- 情報爆発時代における安全・安心ITシステム基盤
- 並列オブジェクト指向言語のマルチコンピュータ上における効率的な実装法
- メッセージ衝突を防止する適応的な収集操作アルゴリズム
- 並列プログラムの実行可搬性を実現するMPI通信ライブラリの設計(インターコネクト/MPI通信ライブラリ,「ハイパフォーマンスコンピューティングとアーキテクチャの評価」に関する北海道ワークショップ(HOKKE-2009))
- DMI:計算資源の動的な参加/脱退をサポートする大規模分散共有メモリインタフェース
- データ集約的ワークフローの高精度なシミュレーター
- XQueryによる柔軟な問い合わせが可能な大規模分散環境モニタリングフレームワーク
- "Bare Metal" Cloud: 実マシンを提供するクラウドサービス
- 広域分散ワークフローのための耐遅延性の高い分散ファイルシステム
- ファイルステージングシステムCatwalkのMPI-IO実装
- 分散共有メモリ環境におけるUCTの並列実行
- 接続を動的に制御するメッセージパッシングシステム(HPC-11 : グリッド(3))(2004年並列/分散/協調処理に関する『青森』サマー・ワークショップ(SWoPP青森2004) : 研究会・連続同時開催)
- 並列アプリケーションのトレースログの効率的なオンライン圧縮アルゴリズムの評価
- ファイルキャッシュシステムの有効性向上に向けた科学技術計算アプリケーションのI/O特性評価
- シームレスなMPI環境を実現するMPI-Adapterの設計と性能評価
- トポロジ情報を用いた効率的かつ漸近安定な大容量ブロードキャスト
- 高いヒープ使用率の下で高速なインクリメンタルGC
- ファイルステージング再考 : オンデマンド化と高速化に向けたプロトタイプ実装の評価(ファイルシステム,「ハイパフォーマンスコンピューティングとアーキテクチャの評価」に関する北海道ワークショップ(HOKKE-2009))
- ファイルステージング再考:オンデマンド化と高速化に向けたプロトタイプ実装の評価 (計算機アーキテクチャ・ハイパフォーマンスコンピューティング・「ハイパフォーマンスコンピューティングとアーキテクチャの評価」に関する北海道ワークショップ(HOKKE-2009))
- 排他的なメソッドの並行な呼び出しを融合する機構を持つ言語
- 同期ボトルネックが存在する並列プログラムの効率的実行(並列処理)
- 明示的なタスク配置指定が可能な遅延タスク生成に基づく動的負荷分散方法
- 動的なスレッド生成をサポートする言語のコンパイル技法
- XQuery による柔軟な問い合わせが可能な大規模分散環境モニタリングフレームワーク
- 6ZA-2 XQueryを用いたプログラマブルかつ軽量な大規模分散環境におけるモニタリングフレームワーク(システム蓮用・管理(2),学生セッション,ネットワーク,情報処理学会創立50周年記念)
- 低負荷で多数の計算機をリアルタイムに監視するシステムVGXPの実装(大規模システム,SWoPP2006)
- Virtual Private Grid(VPG) : 遠隔計算機を効率的に利用するシェル
- 編集にあたって(情報爆発時代におけるわくわくするITの創出を目指して)
- 6ZA-8 広域環境におけるRTTを用いたネットワークトポロジー推定(システム蓮用・管理(2),学生セッション,ネットワーク,情報処理学会創立50周年記念)
- 5W-9 計算機トラブルシュートドメインにおける固有表現抽出(言語情報抽出,学生セッション,人工知能と認知科学,情報処理学会創立50周年記念)
- 4T-2 学習を用いた枝刈の新手法の提案(ゲーム,学生セッション,人工知能と認知科学,情報処理学会創立50周年記念)
- 3L-2 NUMAにおけるメモリローカリティと負荷分散を同時に考慮した並列GCのシミュレーションによる性能評価(分散・並列OS,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 分散計算機環境における異常動作の原因の特定手法(耐エラー技術,SWoPP佐賀2008-2008年並列/分散/協調処理に関する『佐賀』サマー・ワークショップ)
- ネットワークトポロジーを考慮した効率的なバンド幅推定手法(HPC-11:通信,2008年並列/分散/協調処理に関する『佐賀』サマー・ワークショップ(SWoPP佐賀2008))
- 自動取得したネットワーク構成情報に基づくMPI集合通信(HPC-1:MPI,2008年並列/分散/協調処理に関する『佐賀』サマー・ワークショップ(SWoPP佐賀2008))
- 6W-2 画像群中の物品発見における計算量削減手法の提案(画像データベース,学生セッション,人工知能と認知科学)
- 4U-5 Webフォーラムの構文情報を用いたトラブルシュート文書抽出(文書の分類と検索,学生セッション,人工知能と認知科学)
- 2U-3 UCTを用いた訓練初期局面の多様化によるTD学習法の改善(ゲーム・知識ベース,学生セッション,人工知能と認知科学)
- 細粒度マルチスレッディングのための言語処理系技術(2)
- 細粒度マルチスレッディングのための言語処理系技術(1)
- 6ZA-7 大規模ネットワークにおける効率的なバンド幅マップ構築アルゴリズム(システム蓮用・管理(2),学生セッション,ネットワーク,情報処理学会創立50周年記念)
- 大規模ネットワークにおけるバンド幅測定アルゴリズム
- 高速なトポロジ推定 : ネットワークを考慮した並列計算のための基盤として(グリッド)
- 6ZB-4 メッセージ衝突を防止した適応的な集合通信(ネットワーク応用(2),学生セッション,ネットワーク,情報処理学会創立50周年記念)
- 2L-1 並列分散環境上のファイル共有システムの負荷原因探索システム(並列システムソフトウェア,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 並列アプリケーションの性能を損なわないポーリング型のモニタリング
- メッセージ衝突を防止する適応的な集合通信
- 分散計算機環境InTrigger上の資源共有ルールの評価(HPC-6:グリッド,2008年並列/分散/協調処理に関する『佐賀』サマー・ワークショップ(SWoPP佐賀2008))
- InTrigger : 柔軟な構成変化を考慮した多拠点に渡る分散計算機環境(HPC-14 : 分散処理)
- 多拠点に渡る分散計算機環境を効率的にモニタリングするための情報収集と表示(管理機構)
- 論理式の充足可能性問題における変数の依存関係に基づく効率的な変数決定順序(HPC-5: 数値計算アルゴリズム(2))
- 論理式の充足可能性問題の並列化におけるClause共有の効果について(CPSY-2 並列分散プログラミング)(2004年並列/分散/協調処理に関する「青森」サマーワークショップ(SWoPP青森2004))
- 耐故障並列計算を支援する自律的な故障検知機構(高信頼)
- 複数サブネット環境における自律的な故障検知機構(OS-4: 通信システム, 2005年並列/分散/協調処理に関する『武雄』サマー・ワークショップ(SWoPP武雄2005)-研究会・連続同時開催-)
- Phoenixプログラミングモデルにおける故障検知ライブラリ(HPC-11 : グリッド(3))(2004年並列/分散/協調処理に関する『青森』サマー・ワークショップ(SWoPP青森2004) : 研究会・連続同時開催)(2004年並列/分散/協調処理に関する『青森』サマー・ワークショップ(SWoPP青森2004) : 研究会・連続同時開催)
- ハッシングに基づく大規模探索問題の耐故障分散処理手法
- 3ZL-2 ネットワークトポロジを考慮したバンド幅推定の高速化手法(情報爆発時代における安全,安心ネットワーク技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 複雑なグリッド環境で柔軟なプログラミングを実現するフレームワーク
- トポロジを考慮しソース選択を行うデータ転送スケジューラ
- マイグレーションを支援する分散集合オブジェクト
- Javaバイトコード変換による細粒度CPU資源管理
- 共有メモリ並列計算機上の並列ガーベージコレクタの性能予測
- 分散記憶並列計算機における局所ごみ集めのスケジュール方式について(並列処理)
- 最小限のコンパイラサポートによる細粒度マルチスレッディング : 効率的なマルチスレッド言語を実装するためのコスト効率の良い方法(並列処理)
- OpenMPにおけるネストした並列性の実装と評価
- 3ZL-1 自動取得したネットワーク構成情報に基づくMPI集合通信アルゴリズムの改良(情報爆発時代における安全,安心ネットワーク技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 6ZJ-1 並列分散システムにおける異常動作の原因特定のためのログ解析(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 動的にチャネルが増減する環境下での分散スナップショットアルゴリズム
- 広域TCPオーバレイにおけるデッドロックフリールーティング(OS-1:オーバレイネットワーク,2008年並列/分散/協調処理に関する『佐賀』サマー・ワークショップ(SWoPP佐賀2008))
- 広域計算環境用のスケーラブルな高性能通信ライブラリ(HPC-11:通信,2008年並列/分散/協調処理に関する『佐賀』サマー・ワークショップ(SWoPP佐賀2008))
- MPI/GXP : 広域環境用の適応的なメッセージパッシングシステム(HPC-2 : 通信方式)
- 適応スパニングツリーを用いた広域メッセージパッシングシステム用の集合通信(ネットワーク)
- 広域メッセージパッシングシステム用の遅延を考慮した接続管理(HPC-10: 通信ライブラリ)
- インクリメンタルPageRankによる重要Webページの効率的な収集戦略(WWW)
- 高効率なI/O処理が可能な細粒度マルチスレッド処理系のChapelによる評価
- Mogami:高遅延環境において広帯域を達成する分散ファイルシステム
- 重心ボロノイ分割を用いた並列粒子法のための動的負荷分散法
- PARP:プロファイル比較に基づく並列アプリケーションの性能解析
- 高い耐遅延性を持つガウス消去法(HPC-7: 並列数値計算ライブラリ)
- Portableでrobustなglobal garbage collectorの構築について
- 高効率なI/Oと軽量性を両立させるマルチスレッド処理系
- 2A1-B34 100時間ワークショップによる融合教育研究プラットフォームの開発
- 高性能分散計算環境のための認証基盤の設計