| 研究課題/領域番号 |
20K11689
|
|---|
| 研究機関 | 信州大学 |
|---|
研究代表者 |
藤原 洋志 信州大学, 学術研究院工学系, 准教授 (80434893)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| キーワード | アルゴリズム / 数理計画法 / 最適化 / 情報基礎 / 応用数学 |
|---|
| 研究実績の概要 |
(1) ビンパッキング問題は、おのおのサイズが紐づけされたアイテムの列を、なるべく少ない数のビンに詰めることを目的とする最適化問題である。計算機アーキテクチャからロジスティックスに至るまで幅広い応用があり、40 年来計算機科学者の好奇心を刺激し続けてきた有名な問題である。我々は、ビンパッキング問題に対するオンラインアルゴリズムを研究する。ビンパッキング問題に対するオンラインアルゴリズムは通常、競合比という評価尺度を用いてその性能を評価する。しかしながら、オンラインアルゴリズムを設計できても、その競合比を求めることは一般に容易ではない。競合比を求めるための統一的な計算法確立の試みは、これまでほとんどなされてこなかった。本研究において我々は、ある条件下での直接的かつ簡便な競合比の計算法を開発した。我々は結果をまとめて電子情報通信学会英文論文誌Dに投稿し、採録された。
(2) アルゴリズムの正しさの証明は、アルゴリズム理論の研究者の使命といっていい。近年、アルゴリズムの正しさの、より強力な裏付けを確立する方法がさまざまに模索されており、関心を集めている。本来のアルゴリズムの出力とともにその正しさの証拠を出力するように実装する手法や、正しさの証明を形式証明により検証する手法などがある。本研究では、証明支援系 Mizar を用いて、アルゴリズムの正しさの検証を行う。具体的には我々は、部分和問題に対する動的計画法を取り上げる。部分和問題に対する動的計画法は再帰関係に基づいて設計される。我々は、その再帰関係の正しさの証明を Mizar 言語により形式化し検証を行った。我々は形式化した証明を学術雑誌 Formalized Mathematics に投稿し、採録された。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
(1) 我々は、ビンパッキング問題に対するオンラインアルゴリズムを研究する。オンラインアルゴリズムとは、アイテムの列の先頭から1つずつ、それを詰めるビンを確定していくアルゴリズムである。オンラインアルゴリズムの性能は、通常、競合比という評価尺度で測られる。競合比とは、対象となるオンラインアルゴリズムが、「アイテムの列の先頭から1つずつ」のルールを無視した詰め方での最小のビン数の何倍のビンを使いうるかを表す。本研究において我々は、アイテムサイズが有限集合であり、補集合に関するある性質を満たし、かつ、オンラインアルゴリズムの要するビン数が、漸近的に各サイズのアイテム数の定数倍の最大値に等しい場合に着目した。そしてその場合に、オンラインアルゴリズムの競合比を、後者の定数から計算できることを証明した。
(2) 本研究では、証明支援系 Mizar を用いて、部分和問題に対する動的計画法の正しさの検証を行う。この動的計画法は、Garey と Johnson の著書 "Computers and Intractability: A Guide to the Theory of NP-Completeness" も取り上げる古典的なアルゴリズムであり、擬多項式時間アルゴリズムの代表例でもある。動的計画法は、解きたい問題を部分問題に分割する。そして、それぞれの部分問題を直接解くかわりに、より小さな部分問題の解を利用することによって解く。その際に最も重要なのが、部分問題の解どうしの再帰関係である。本研究にて我々は、部分和問題に対する動的計画法の再帰関係の正しさ、およびそのために必要な補題を Mizar 言語により記述し、チェッカプログラムにかけることにより検証を行った。
|
| 今後の研究の推進方策 |
(1) 我々が開発した競合比の計算法は、有名な HARMONIC アルゴリズムを適用対象に含むなど、広範囲のオンラインアルゴリズムを扱うことができる。実際に、電子情報通信学会英文論文誌Dに掲載した論文上でも、そのデモンストレーションを行っている。しかしながら我々は、オンラインアルゴリズムに関する適用条件についてはまだまだ緩和の余地があると信じている。適用条件の緩和は、計算の汎用性を飛躍的に高める。我々はその手始めとして、オンラインアルゴリズムが生成するビン数の凸性や斉次性に着目して、どのように適用条件を緩和をできるか検討する。
(2) 我々は、部分和問題に対する動的計画法の再帰関係の正しさを形式化した。今後の推進方策として、大きく分けて2つのことが挙げられる。1つは、動的計画法から得られる解が、部分和問題に対する最適解の1つである性質の形式化である。これは、現在までの進捗であと一歩のところまで来ており、残るは Mizar のファンクターの存在性と唯一性の証明のみである。もう1つは、部分和問題に対する動的計画法を Mizar の状態機械上のアルゴリズムとして形式化することである。Mizar にはすでに形式化された状態機械がある。我々がこれまでに行った再帰関係の形式化によりアルゴリズムの正しさは保証されたが、その状態遷移を形式化することにより、アルゴリズムの実行の各状態を検証可能にしたいと考えている。
|
| 次年度使用額が生じた理由 |
当初計画では、ビンパッキング問題に関する研究発表のための出張および学術論文の投稿を令和2年度に実施予定であったが、研究の進捗状況により、令和3年度に実施することとしたため、次年度使用額が生じた。
(使用計画)
・次年度使用額は、令和3年度請求額と合わせて旅費および論文掲載料として使用する。
|
