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

1999 Fiscal Year Annual Research Report

• Project/Area Number: 09480055
• Research Institution: KYOTO UNIVERSITY
• Principal Investigator: 岩間 一雄 京都大学, 大学院・情報学研究科, 教授 (50131272)
• Co-Investigator(Kenkyū-buntansha): 荻野 博幸 京都大学, 大学院・情報学研究科, 助手 (40144323) ; 安岡 孝一 京都大学, 大型計算機センター, 助教授 (20230211) ; 岡部 寿男 京都大学, 大学院・情報学研究科, 助教授 (20204018) ; 岩本 宙造 広島大学, 工学部, 助教授 (60274495) ; 宮崎 修一 京都大学, 大学院・情報学研究科, 助手 (00303884)
• Keywords: 実世界問題 / 充足可能性問題 / 部分MAXSAT / 学生配属問題 / 局所探索アルゴリズム / 並列化 / ベクトル化 / PVM

Research Abstract

複雑なデータ構造を持つ実世界の組合せ最適化問題に対して,効率的な解法を構築するというのが本研究の目的である.本研究では個々の問題を直接解くのではなく,一旦和積形論理式の充足可能性問題(SAT)に変換し,SATに対する高速アルゴリズムを利用して元の問題を解くというアプローチをとる.本手法の利点は次の通りである.(1)SATは記述能力に優れており,様々な問題からSATへの変換は容易に行なうことができる.(2)SATに対する既存の高速アルゴリズムを利用することができる.
昨年度までは,実世界問題の定式化を行ない,この定式化された実世界問題からSATへの統一的な変換手法を示した.また,本手法の有効性を示すために,時間割作成.学生配属という,大学で最も需要の高いと思われる最適化問題に対して計算機実験を行なった.いずれの問題に対しても,既存の直接解法アルゴリズムよりも我々の手法の方が良い解を得られることを示すことができた.
本年度は,SATに対する局所探索法の高速化を行なった.本研究では,ベクトル計算機とPVMを利用して,並列化による高速化を行なった.局所探索アルゴリズムは,それぞれの探索を独立に行なうことができるので,非常に並列化に向いている.しかも、並列アルゴリズム特有の通信によるオーバーヘッドがほとんどないため,理想的な台数効果が得られるものと期待した.実験により,期待通りの高速化が実現できたことを確かめた.さらに,ベンチマーク例題を利用して性能評価を行なったところ,これまでどのプログラムによっても解かれていなかったいくつかの例題を解くことができた.

Research Products

• [Publications] Amano M.: "Undecidability on Quantum Finite Automata"Proc. STOC'99. 368-375 (1999)
• [Publications] Iwama K.: "Stable Marriage with Incomplete Lists and Ties"Proc. ICALP'99. 443-452 (1999)
• [Publications] Iwama K.: "Multipacket routing on 2-D meshes and its applications to fault-tolerant routing"Proc. ESA'99. 53-64 (1999)
• [Publications] Iwama K.: "Using Generalized Forcasts for Online Currency Conversion"Proc. COCOON'99. 409-421 (1999)
• [Publications] Iwama K.: "Tree-Like Resolution Is Superpolynomially Slower Than DAG-Like Resolution for the Pigeonhole Principle"Proc. ISAAC'99. 133-142 (1999)
• [Publications] Asahiro Y.: "Greedily Finding a Dense Subgraph"J. Algorithms. 34. 203-221 (2000)