2021 Fiscal Year Annual Research Report
Studies toward disproving the strong exponential time hypothesis
Project/Area Number |
18K11170
|
Research Institution | Hokkaido University |
Principal Investigator |
脊戸 和寿 北海道大学, 情報科学研究院, 准教授 (20584056)
|
Co-Investigator(Kenkyū-buntansha) |
長尾 篤樹 お茶の水女子大学, 基幹研究院, 助教 (20802622)
|
Project Period (FY) |
2018-04-01 – 2022-03-31
|
Keywords | 強指数時間仮説 / 充足可能性問題 / 厳密アルゴリズム |
Outline of Annual Research Achievements |
本研究の目的は和積標準形論理式における充足可能性問題を全探索より指数的に高速に解くアルゴリズムは存在しないという強指数時間仮説を否定するための研究を実施することであった。延長期間を含めた4年間の研究で様々な知見を得ることができたが、実際に否定するためのアルゴリズム構築には至らなかった。当初の目標として、強指数時間仮説と同等の仮説を立てることも挙げていたが、今後の研究につながるような仮説を立てることはできなかった。 しかし、これらの研究過程において、k 回読み分岐プログラムの充足可能性判定アルゴリズムやノード数が変数の数の線形個である幅2分岐プログラムの充足可能性判定アルゴリズムを構築することができた。これらのアルゴリズムは全探索よりも指数的に高速に動作する。このことは、k 回読み分岐プログラムや線形サイズの幅2分岐プログラムで表現可能な和積標準形論理式上では強指数時間仮説が成り立たないことを示唆している。その結果、これらのモデルでは表現できない論理式上の充足可能性問題を考える必要があることがわかった。 2021年度の最終年度は、先に挙げた、変数の数の線形個のノードをもつ幅2分岐プログラムの充足可能性判定アルゴリズムを構築することに成功した。このアルゴリズムは全探索よりも指数的に高速に動作するアルゴリズムである。また、アルゴリズム構築の過程で、さらに改良可能な方法も発見できたが、それには別の性質をもつ充足可能性問題を解くアルゴリズムを構築する必要があるため、2021年度内に改良はできなかった。
|