| 研究実績の概要 |
制約充足問題は様々な分野に現れる普遍的な組合せ問題である．一般的な制約充足問題に対する効率的なアルゴリズムは存在しないと考えられている．そのような計算困難問題に対するアルゴリズムを設計するためのアプローチとして，特殊な問題にのみ動くアルゴリズム，厳密アルゴリズム，近似アルゴリズムがある．これら3種類のアプローチは従来ほとんど独立に研究されてきた．本課題では，3種類のアプローチを融合することで，制約充足問題に対する，より効率の良い厳密および近似アルゴリズムの設計とその解析を行うことを目的とする．制約充足問題の個々のクラスに対するアルゴリズムの開発を行うことで得られた知見を生かし，広範なクラスに対する汎用的なアルゴリズムを開発することが最終的な目標である．以下に本年度の主要な成果を述べる.
本研究では, 素子除去と呼ばれる方法に基づき, 論理回路に対する最悪時/平均時計算困難性証明および充足可能性判定アルゴリズムを統一的に与える枠組みを構築した. 素子除去とは, 論理回路の入力を制限した際に冗長となる素子を取り除くことをいう. 例えば, 変数の値を固定したり, 変数間に線形制約を課したりすることで, 冗長な素子が生じる. 素子除去は計算困難性証明や充足可能性判定でよく用いられる手法であるが, その適用や解析は扱う問題に応じて調節が必要である. 本研究では, 素子除去の効率さえ証明できれば計算困難性証明や充足可能性判定の効率が自動的に従うことを示せた. その帰結として, 既存より大きい素子数の下界証明と高速な判定アルゴリズムを得た.
|
