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

1998 Fiscal Year Annual Research Report

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

Research Abstract

複雑なデータ構造を持つ実世界の組合せ最適化問題に対して,効率的な解法を構築するというのが本研究の目的である.本研究では個々の問題を直接解くのではなく,一旦和積形論理式の充足可能性問題(SAT)に変換し,SATに対する高速アルゴリズムを利用して元の問題を解くというアプローチをとる.本手法の利点は次の通りである.(1)SATは記述能力に優れており,様々な問題からSATへの変換は容易に行なうことができる.(2)SATに対する既存の高速アルゴリズムを利用することができる.昨年度は大学の時間割作成問題を例にとり,この方法の有効性を明らかにした.また,部分MAXSATという新たな最適化問題を導入し,実世界問題を模倣するのに部分MAXSATがより有効であることを示した.
本年度は,上述の(1)の部分に重点をおいて研究を行なった.SATへの変換は容易であるとは言え,誰もが与えられた問題を簡単にSATに変換できるとは言い難い.そこで,本研究の手法を幅広く使えるようにするために,実世界の組合せ問題からSATへの変換を行なうための指針を与えることを本年度の目標とした.
本研究ではまず,実世界問題の枠組を定式化した.この枠組は,2つの集合の間の写像の形でなされており,上述の時間割問題はもちろん,様々な最適化問題を記述できる一般的なものである.次に,実世界問題からSATへの変換手法を確立した.これにより,組合せ問題を実世界問題の枠組で記述できさえすれば,SATへの変換はほぼ自動的に行なえるようになった.
また,具体的例題として,大学院学生を研究室に配属する学生配属問題を取り上げ,我々の手法により問題を解くことを試みた.すなわち,学生配属問題を実世界問題の枠組で記述し,SATへ自動的に変換を行ない,SATの解から配属を求めた.自動鰺な変換方法を用いることにより,サイズを多少増大してしまうが,高速なSATアルゴリズムにより元の問題の良質の解を求められることが分かった.また,変換方法を個々の特徴に合わせて工夫することにより,問題のサイズの増大を抑えられることも分かった.

Research Products

• [Publications] Kazuo Iwata: "Efficient Randomized Routing Algorithms on the Two-Bimensional mesh of buses" Proc.COCOON'98(LNCS 1449). 229-240 (1998)
• [Publications] Kazuo Iwama: "New Bounds for Oblivious Mesh Routing" Proc.ESA'98(LNCS 1461). 295-306 (1998)
• [Publications] Kazuo Iwama: "Improved Time and Space Hierarchies of One-Tape Off-Line TMs" Proc.MFCS'98(LNCS 1450). 580-588 (1998)
• [Publications] Kazuo Iwata: "Optimizing OBDDs Is Still Intractable for Monotone Functions" Proc.MFCS'98(LNCS 1450). 625-635 (1998)
• [Publications] Kazuo Iwama: "An O(√<N>)Oblivious Routing Algorithms for 2-D Meshes of Constant Queue-Size" Proc.SODA'99. 466-475 (1999)
• [Publications] Masami Amano: "Undecidability on Quantum Finite Automata" Proc.STOC'99. (発表予定). (1999)