文献

J-GLOBAL ID：201502213852166634   整理番号：15A1192322

SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価

著者 (4件)： 川原征大 (神戸大 大学院システム情報学研究科) ,  宋剛秀 (神戸大 情報基盤セ) ,  番原睦則 (神戸大 情報基盤セ) ,  田村直之 (神戸大 情報基盤セ)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 32nd  ページ： ROMBUNNO.PPL3-1  発行年： 2015年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 部分グラフ探索とは,与えられたグラフから制約を満たす部分グラフを見つけることであり,回路配線等の様々な応用が知られている。本論文では,SATソルバーを用いた高速な部分グラフ探索ツールを提案・評価する。既存研究としてはZero-suppressed decision diagram(ZDD)を用いた部分グラフ探索ツールGraphillionがある。ZDDは解の数が多くなっても高速に全列挙可能という特長を持つが,大きなグラフではZDDの構築に失敗することがある。一方,SATソルバーは大規模な問題に対しても,高速な単解探索が可能であるという特長を持つ。本研究ではまず部分グラフ探索で使われるグラフ上の制約のSAT符号化方法を提案する。特に頂点の連結性に関する制約モデルについては推移関係を用いた方法と次数の制約を用いた方法の2種類を提案する。計算機実験の結果,kクリーク問題,マルチパス問題,ハミルトン閉路の単解探索において,ZDDが利用不可能な1000頂点以上のグラフでも高速に求解できることを確認した。(著者抄録)

シソーラス用語： *制約充足問題 ,  *グラフ理論 ,  応用プログラム ,  高速度 ,  部分グラフ ,  探索問題 ,  制約条件 ,  配線 ,  集積回路 ,  性能評価 ,  クリーク ,  Hamilton閉路
準シソーラス用語： 高速ソルバ ,  集積回路配線

分類 (2件)： 論理代数  (JB03000H) ,  グラフ理論基礎  (IA02020S)

タイトルに関連する用語 (7件)： SAT ,  ソルバー ,  部分グラフ ,  探索 ,  ツール ,  実装 ,  評価