高速SATアルゴリズムを利用した実世界組合せ問題の統一的解法

閲覧数: 6
ダウンロード数: 0
このエントリーをはてなブックマークに追加

高速SATアルゴリズムを利用した実世界組合せ問題の統一的解法

フォーマット:
助成・補助金
Kyushu Univ. Production 九州大学成果文献
タイトル(他言語):
Solving Real-World Combinatorial Problems using High-Speed SAT-Algorithms
責任表示:
岩間 一雄(京都大学・情報学研究科・教授)
IWAMA Kazuo(京都大学・情報学研究科・教授)
本文言語:
日本語
研究期間:
1997-1999
概要(最新報告):
複雑なデータ構造を持つ実世界の組合せ最適化問題に対して,効率的な解法を構築するというのが本研究の目的である.本研究では個々の問題を直接解くのではなく,一旦和積形論理式の充足可能性問題(SAT)に変換し,SATに対する高速アルゴリズムを利用して元の問題を解くというアプローチをとる.本手法の利点は次の通りである.(1)SATは記述能力に優れており,様々な問題からSATへの変換は容易に行なうことができる.(2)SATに対する既存の高速アルゴリズムを利用することができる. 本研究では,まず,実世界問題の定式化を行ない,この定式化された実世界問題からSATへの統一的な変換手法を示した.これにより,与えられた問題をSATに自動的に変換することが可能となった. 次に,本手法の有効性を示すために,時間割作成,学生配属という,大学で最も需要の高いと思われる最適化問題に対して計算機実験を行なった.いずれの問題に対しても,既存の直接解法アルゴリズムよりも我々の手法の方が良い解を得られることを示すことができた. 最後に,SATに対する局所探索法の高速化を行なった.本研究では,ベクトル計算機とPVMを利用して,並列化による高速化を行なった.局所探索アルゴリズムは,それぞれの探索を独立に行なうことができるので,非常に並列化に向いている.しかも,並列アルゴリズム特有の通信によるオーバーヘッドがほとんどないため,理想的な台数効果が得られるものと期待した.実験により,期待通りの高速化が実現できたことを確かめた.さらに,ベンチマーク例題を利用して性能評価を行なったところ,これまでどのプログラムによっても解かれていなかったいくつかの例題を解くことができた. 続きを見る
本文を見る

類似資料:

2
定理自動証明技術の計算論的研究 by 岩間 一雄; IWAMA Kazuo
8
JavaによるSATソルバHerrsatの実装と学習節の削減法について by 大森, 晋作; Omori, Shinsaku; 松下, 幸之助; Matsushita, Konosuke; 長谷川, 隆三; Hasegawa, Ryuzo; 藤田, …
11
クライアント‐サーバモデルによる評価済み核データライブラリの利用 by 河野, 俊彦; 酒井, 治; 中島, 秀紀; Kawano, Toshihiko; Sakai, Osamu; Nakashima, Hideki
6
DPLL型SATソルバを用いた極小モデル生成について by 鹿田, 憲秀; Shikada, Norihide; 谷口, 清則; Taniguchi, Kiyonori; 長谷川, 隆三; Hasegawa, Ryuzo; 藤田, 博; …
2.
定理自動証明技術の計算論的研究 by 岩間 一雄; IWAMA Kazuo
6.
DPLL型SATソルバを用いた極小モデル生成について by 鹿田, 憲秀; Shikada, Norihide; 谷口, 清則; Taniguchi, Kiyonori; 長谷川, 隆三; Hasegawa, Ryuzo; 藤田, 博; …
8.
JavaによるSATソルバHerrsatの実装と学習節の削減法について by 大森, 晋作; Omori, Shinsaku; 松下, 幸之助; Matsushita, Konosuke; 長谷川, 隆三; Hasegawa, Ryuzo; 藤田, …
11.
クライアント‐サーバモデルによる評価済み核データライブラリの利用 by 河野, 俊彦; 酒井, 治; 中島, 秀紀; Kawano, Toshihiko; Sakai, Osamu; Nakashima, Hideki