| 研究概要 |
定理証明系の複雑さの解析を行なうことを目的とし,導出原理の複雑さに関する研究を行なった.導出原理とは,和積形論理式が恒偽であることを証明する証明系である.本年度は以下の結果を得た.
(1)導出原理による証明を見つける問題は盛んに議論されており,証明を見つけるための高速なアルゴリズムも近年発見されている.本研究では,本問題を最適化の面から議論した.すなわち,できるだけ短い証明を見つける問題の複雑さを議論した.その結果,n変数の論理式の最短の証明の長さをSとしたとき,任意の定数dに対し,長さS+O(n^d)以下の証明を見つける問題がNP困難であるという結果を得た.
(2)導出原理とバックトラック法の関係について論じた.バックトラック法とは,CNF論理式の充足可能性問題(SAT)に対する深さ優先探索アルゴリズムである.本研究では,導出原理の証明木からバックトラック法の探索木が,また逆にバックトラック法の探索木から導出原理の証明木が,サイズを増やさずに得られることが分かった.証明や探索が木でなく有効グラフになっている場合については現在検討中である.
(3)冗長度を増すことにより,証明時間を極端に減らすことができる例を発見した.あるグラフ問題をSATに変換して得られた論理式に対し,そのままでは証明に指数ステップを要する(ことが予想される)が,冗長な項を少数追加することによって,多項式時間で証明することができる.他の問題をSATに変換して解く場合,式のサイズを小さくすることが効率の上昇に継ると考えられているが,本結果は,ある程度の冗長度を含ませることも重要である場合があることを示唆している.
|
