| 研究概要 |
理論計算機科字分野における大きな未解決問題の1つに,NP対coNP問題があげられる.この問題に対する重要なアプローチ法に証明の複雑さの研究がある.証明の複雑さとは,与えられた論理式が恒真式であることを,公理から始め,推論規則を用いることで証明するときに(このような公理と規則をもつ機構を証明系とよぶ),必要とされる証明のサイズを,入力される式のサイズの関数として求める研究である.証明系の中でも非常に強力であるExtended FregeSystemに対する超多項式下界を求めることは,現存の手法のみでは非常に困難である.本研究では,Extended Fregeと等価な能力をもつ,Hajos Calculusというグラフ計算論法を用いることで,従来の論理式を用いた手法とは異なる,グラフ理論的アプローチによる下限証明の研究を行う.HajosCalculusとは,3彩色不能なグラフを4頂点の完全グラフから始め,3つのルールの1つを非決定的に適用していくことで,新たな3彩色不能なグラフを生成していくグラフ計算論法である.Hajos Calculusにおいて多項式ステップで構成困難なグラフを発見することは長年に渡る非常に重要な未解決問題である.
本年度は,前年度までにアルゴリズムの考案とプログラムによる実装を行っていた3彩色不能な平面グラフを列挙することが可能な列挙アルゴリズムの改良と高速化を中心に研究を行った.この列挙アルゴリズムはHajos Calculusを部分的にシミュレートする列挙アルゴリズムであり,下界証明の手がかりとして有用であると考えている.このアルゴリズムを列挙アルゴリズムで用いられる様々な技法を用いて改良し,列挙の高速化をさせることに成功した.
|
