双対モデリングを用いた充足可能性問題のCNF encoding
スポンサーリンク
概要
- 論文の詳細を見る
充足可能性問題(SAT)とは、与えられた論理式に対して充足可能な変数割り当てがあるかどうか証明する問題である。近年の研究の成果により、問題を解決するソルバが著しく発展し、回路検証やモデル検査などの実アプリケーションに応用が期待されている。本研究では、このSATソルバに入力として与える乗法標準形(CNF)に着目し、効率よく解くことのできるCNFの作成手法の確立を目指す。具体的には、SATと関連の深い制約充足問題(CSP)で発案された双対モデリングの手法をSATのCNF encodingに適用し様々な評価実験を行った。巡回セールスマン問題を含む三つの問題を取り上げ、大きな探索空間が必要な問題に対して効果的であり、SAT問題における双対モデリングの有効性や特性を捉えることができた。
- 2008-09-05
著者
-
稲葉 真理
東京大学大学院情報理工学系研究科
-
上田 和紀
早稲田大学理工学部情報学科
-
稲葉 真理
東大
-
稲葉 真理
東京大学情報理工学系研究科
-
薗部 知大
東京大学大学院情報理工学系研究科
-
稲葉 真理
東京大学理学系研究科
-
稲葉真理
東京大学
-
上田 和紀
早稲田大学大学院情報理工学専攻
-
上田 和紀
早稲田大学
-
稲葉 真理
東京大学大学院情報理工学研究科
関連論文
- パケット喪失履歴に基づいたTCP輻輳制御方式 (コンピュータシステム)
- ハードウェア・エンジンを用いた10GbE上のTCP通信解析(HPC-17 : 高性能通信)
- FPGA基板を用いたモンテカルロ碁の高速化(アクセラレーションと回路設計,2009年並列/分散/協調処理に関する『仙台』サマー・ワークショップ(SWoPP仙台2009))
- 並列計算機システムFOLON上へのPVMの移植と評価
- 並列TCPストリーム間協調を目的とした流量調整機構Stream Equalizerの性能評価(HPC-11:通信,2008年並列/分散/協調処理に関する『佐賀』サマー・ワークショップ(SWoPP佐賀2008))
- 細粒度パケット間隔制御の実装と評価(OS-4: 通信システム, 2005年並列/分散/協調処理に関する『武雄』サマー・ワークショップ(SWoPP武雄2005)-研究会・連続同時開催-)
- インテリジェントNICを用いた高帯域ネットワーク向けTCP通信方式(OS-3:ネットワーク)(2004年並列/分散/協調処理に関する『青森』サマー・ワークショップ(SWoPP青森2004) : 研究会・連続同時開催)
- 双対モデリングを用いた充足可能性問題のCNF encoding
- 微分制約論理式によるハイブリッドシステムのモデリングと検証
- なぜソフトウェア論文を書くのは難しい(と感じる)のか
- 3A-1 大規模メモリ環境下におけるモデル検査ツールSpinのマルチコア検証機能の性能評価(高性能計算,一般セッション,アーキテクチャ)
- 3A-2 強連結成分ベースのグラフ分割による分散並列LTLモデル検査の高速化(高性能計算,一般セッション,アーキテクチャ)
- 6ZJ-9 階層グラフ書換え言語LMNtalによるモデル検査(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 4K-2 分散検証環境DiVinEを用いた分散LTLモデル検査アルゴリズムの性能評価(情報爆発時代における分散処理とセキュリティ,一般セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 簡潔データ構造による全文検索のハードウェアを用いた高速化(ハードウェアアクセラレーション,SWoPP佐賀2008-2008年並列/分散/協調処理に関する『佐賀』サマー・ワークショップ)
- Internet2 Land Speed Record : 長距離TCP通信高速化への挑戦
- 超高速インターネット通信におけるFPGA技術の利用(超並列SIMDプロセッサ,先端的コンピュータシステム技術及び一般)
- ゲートウェイによる並列TCPのウィンドウサイズ平均化(HPC-15 : ネットワーク)
- Sakura-C : 超並列計算機向けC言語と最適化(HPC-1 : 最適化)
- 6ZJ-7 並列SATソルバにおけるlemma共有およびプール制約伝播高速化(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- SATソルバ MiniSat の並列化とそのチューニング手法(HPC-2 : 数値解析I)
- SIMD型計算機向けループ自動並列化手法
- Webブラウザを用いた長距離データ転送の高速化
- A-022 数式処理システムMathematica上における再帰除去システム(A分野:モデル・アルゴリズム・プログラミング)
- 幾何クラスタリングとデータマイニング
- Ruby用仮想マシンにおけるAOTコンパイラ
- マップ型履歴を用いたプリフェッチ方式とキャッシュ置換方式の協調動作
- トピックス
- プロファイルを使用した並列LTLモデル検査のチューニング
- ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法
- A-007 区間演算を用いたODE Solverにおける任意精度演算の導入とパラメタ最適化(モデル・アルゴリズム・プログラミング,一般論文)
- ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法
- 超並列準汎用計算機GRAPE-DRによる重力多体問題シミュレーションおよびLU分解
- LMNtalモデル検査器における状態爆発対策(高信頼化,2010年並列/分散/協調処理に関する『金沢』サマー・ワークショップSWoPP2010)
- 強連結成分の特性を用いた並列モデル検査アルゴリズムSCC-OWCTYの設計と評価(高信頼化,2010年並列/分散/協調処理に関する『金沢』サマー・ワークショップSWoPP2010)
- 日米間QoSによるLFN高速化実験と分散KVSの構築(研究発表,ネットワーク研究開発テストベッド運用・利用,一般)
- ソフトウェア論文座談会
- TCPによる長距離ディスク間データ転送の高速化
- Computational Geometry on Statistical Manifolds for Clustering : Extended Abstract (Models of Computation and Algorithms)
- 省ハードウェア資源のフィードバックつきハイブリッドプリフェッチ方式
- 省ハードウェア資源のフィードバックつきハイブリッドプリフェッチ方式
- フィードバックを用いたハイブリッド・プリフェッチ方式
- 長距離広帯域ネットワークでのTCP/IP Acknowledge Packet受信の影響ついて(インターネット応用及び一般)
- 長距離広帯域ネットワークでのTCP/IP Acknowledge Packet受信の影響ついて(インターネット応用及び一般)
- 10ギガビットネットワーク上での高効率TCP/IP通信の実現(HPC-17 : 高性能通信)
- Real Long Fat NetworkにおけるTCP/IPv6の通信性能評価(インターネット及び一般)
- Real Long Fat NetworkにおけるTCP/IPv6の通信性能評価(インターネット及び一般)
- FLASHを用いたリアルタイム講演中継システムとその特性(インターネット運用・管理技術,一般,インターネット運用・管理技術,一般)
- 擬似ネットワーク環境におけるTCP/IPの性能評価(インターネット及び一般)
- 擬似ネットワーク環境におけるTCP/IPの性能評価(インターネット及び一般)
- TCPストリームによる世界最長10ギガビット高速通信回線実験 : Internet2 Land Speed Recordへの挑戦(インターネット・フォトニックネットワークアプリケーション, 一般)
- TCPストリームによる世界最長10ギガビット高速通信回線実験 : Internet2 Land Speed Record への挑戦
- 高レイテンシ環境下におけるデータレゼボワールの性能評価
- MK-4 Data Reservoir : 科学技術研究向け超高速ネットワーク基盤(大型プロジェクト紹介,学術系企画)
- 超高速ネットワーク用データ共有システム : データレゼボワールの性能評価
- Data Reservoirプロトタイプシステム : アプローチと実験結果
- Data Reservoir : 理学研究のための新しい超高速ネットワーク利用基盤
- 階層グラフ書換え言語LMNtalの処理系(ソフトウェア論文)
- 省ハードウェア資源のフィードバックつきハイブリッドプリフェッチ方式
- 省ハードウェア資源のフィードバックつきハイブリッドプリフェッチ方式
- LMNtal処理系および他言語インタフェースの設計と実装
- パケット喪失履歴に基づいたTCP幅輳制御方式(2010年並列/分散/協調処理に関する『金沢』サマー・ワークショップSWoPP2010)
- CometインテリジェントNICの応用(第1版)(ネットワーク・インターネット基礎,産学連携論文)
- Comet インテリジェントNICの応用(第1版)
- 超並列準汎用計算機GRAPE-DRによる重力多体問題シミュレーションおよびLU分解
- 協調動作する並列TCPストリームへのPacket Spacingの適用とその評価(HPC-10 : ネットワークとスケジューリング)(2004年並列/分散/協調処理に関する『青森』サマー・ワークショップ(SWoPP青森2004) : 研究会・連続同時開催)
- ギガビットイーサネット上での遠距離TCP通信におけるPacket Spacing(インターネット関連技術,及び一般)
- ギガビットイーサネット上での遠距離TCP通信におけるPacket Spacing(インターネット関連技術,及び一般)
- 地理情報システムの標準化動向と参照モデル
- 超並列SIMDマシン上でのMIMDプログラム実行スケジューリング最適化(大規模システム,SWoPP2006)
- flat-c: 超並列計算機向けC言語の実現(HPC-9: 並列プログラミング)
- 制約に基づく解析による並行論理プログラムの自動デバッグ
- 6K-4 LMNtal処理系SLIMのモデル検査機能の並列化(情報爆発時代における並列分散処理技術,一般セッション,「情報爆発」時代に向けた新IT基盤技術,情報処理学会創立50周年記念(第72回)全国大会)
- 6K-2 クラスタ向け並列precosatの開発と性能評価(情報爆発時代における並列分散処理技術,一般セッション,「情報爆発」時代に向けた新IT基盤技術,情報処理学会創立50周年記念(第72回)全国大会)
- 1M-1 ハイブリッドシステムモデリング言語HydLaの区間制約に基づく全解シミュレーション実行処理系(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 論理・制約プログラミングと並行計算(論理と推論技術の展開)
- 特集「論理と推論技術の展開」の編集にあたって
- 6ZJ-8 軽量なLMNtal実行時処理系SLIMの設計と実装(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 4N-2 KLICへのデータ並列処理機能の導入について
- 3K-2 汎用並列組合せ最適化パッケージの構想
- C. A. R. Hoare : Communicating Sequential Processes(20世紀の名著名論)
- シンガポール国立大学
- 私はCrusoeを使いたい(インタラクティブ・エッセイ)
- RL-001 FPGAを用いた広帯域高遅延ネットワーク向けの利用可能帯域推定(L分野:ネットワーク・セキュリティ,査読付き論文)
- 長距離・短距離通信が混在する環境でのTCP/IPのデータ転送速度の理論的解析
- A-014 LMNtalコンパイラにおける並び替えとグループ化を用いた命令列の最適化(A分野:モデル・アルゴリズム・プログラミング)
- 並列計算機システムFOLONの通信ライブラリの設計と評価
- 見込み計算を用いたニュースリーダの応答性改善法
- MK-5 戦略ソフトウェア創造人材養成プログラム(大型プロジェクト紹介,学術系企画)
- ランダマイズドクラスタリングアルゴリズムに関する実験結果について
- BDDを用いたデータマイニング
- HPC Ruby:静的解析に基づくRubyの高度最適化コンパイラ
- BTBへのBimode Cascading手法適用による分岐先アドレス予測の高効率化
- 多様な履歴の利用による分岐予測精度の向上
- 実用的なRuby用AOTコンパイラ
- 並列TCPストリームのための流量割り当て方式(HPC-2 : 通信方式)
- 動的再構成を用いたアプリケーションレイヤ処理エンジンの設計(ネットワーク, デザインガイア-VLSI設計の新しい大地を考える研究会-)
- バンド幅チャレンジとネットワーク背景技術
- 情報検索・全文データベースでの文書クラスタリングでの幾何構造活用
- データマイニングでのクラスタリング