| 研究分担者 |
PAUL Purdom インディアナ大学, 計算機科学科, 教授
RUSSELL Impa カリフォルニア大学(サンジエゴ校), 計算機科学科, 助教授
櫻井 幸一 (桜井 幸一) 九州大学, 大学院・システム情報科学研究科, 助教授 (60264066)
TONIANN Pita アリゾナ大学, 計算機科学科, 助教授
IMPAGLIAZZO ラッセル カリフォルニア大学(サンジエゴ校), 計算機科学科, 助教授
PITASSI Toni アリゾナ大学, 計算機科学科, 助教授
|
|---|
| 研究概要 |
人工知能分野の基本的テーマである定理の自動証明は,多くの研究者の興味を引いて来たが,基礎的な解析が進んでいないため未だ実用化の目度が立っていない.本研究では定理証明系の複雑さの解析を行なうことを目的とし,導出原理の複雑さに関する研究を行なった.導出原理とは,和積形論理式が恒偽であることを証明する証明系である.本テーマに関して,以下結果を得た.
(1)導出原理による証明を見つける問題は盛んに議論されており,証明を見つけるための高速なアルゴリズムも近年発見されている.本研究では,本問題を最適化の面から議論した.すなわち,できるだけ短い証明を見つける問題の複雑さを議論した.その結果,n変数の論理式の最短の証明の長さをSとしたとき,任意の定数dに対し,長さS+O(n^d)以下の証明を見つける問題がNP困難であるという結果を得た.
(2)導出原理とバックトラック法の関係について論じた.バックトラック法とは,CNF論理式の充足可能性問題(SAT)に対する深さ優先探索アルゴリズムである.本研究では,導出原理の証明木からバックトラック法の探索木が,また逆にバックトラック法の探索木から導出原理の証明木が,サイズを増やさずに得られることが分かった.
(3)冗長度を増すことにより,証明時間を極端に減らすことができる例を発見した.あるグラフ問題をSATに変換して得られた論理式に対し,そのままでは証明に指数ステップを要する(ことが予想される)が,冗長な項を少数追加することによって,多項式時間で証明することができる.他の問題をSATに変換して解く場合,式のサイズを小さくすることが効率の上昇に継ると考えられているが,本結果は,ある程度の冗長度を含ませることも重要である場合があることを示唆している.
|
