1997 Fiscal Year Annual Research Report
| Project/Area Number |
08044158
|
|---|
| Research Institution | KYOTO UNIVERSITY |
|---|
Principal Investigator |
岩間 一雄 京都大学, 工学研究科, 教授 (50131272)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
IMPAGLIAZZO ラッセル カリフォルニア大学(サンジエゴ校), 計算機科学科, 助教授
桜井 幸一 九州大学, 大学院・システム情報科学研究科, 助教授 (60264066)
PITASSI Toni アリゾナ大学, 計算機科学科, 助教授
|
|---|
| Keywords | 定理証明 / 導出原理 / 計算複雑さ |
|---|
| Research Abstract |
定理証明系の複雑さの解析を行なうことを目的とし,導出原理の複雑さに関する研究を行なった.導出原理とは,和積形論理式が恒偽であることを証明する証明系である.本年度は以下の結果を得た.
(1)導出原理による証明を見つける問題は盛んに議論されており,証明を見つけるための高速なアルゴリズムも近年発見されている.本研究では,本問題を最適化の面から議論した.すなわち,できるだけ短い証明を見つける問題の複雑さを議論した.その結果,n変数の論理式の最短の証明の長さをSとしたとき,任意の定数dに対し,長さS+O(n^d)以下の証明を見つける問題がNP困難であるという結果を得た.
(2)導出原理とバックトラック法の関係について論じた.バックトラック法とは,CNF論理式の充足可能性問題(SAT)に対する深さ優先探索アルゴリズムである.本研究では,導出原理の証明木からバックトラック法の探索木が,また逆にバックトラック法の探索木から導出原理の証明木が,サイズを増やさずに得られることが分かった.証明や探索が木でなく有効グラフになっている場合については現在検討中である.
(3)冗長度を増すことにより,証明時間を極端に減らすことができる例を発見した.あるグラフ問題をSATに変換して得られた論理式に対し,そのままでは証明に指数ステップを要する(ことが予想される)が,冗長な項を少数追加することによって,多項式時間で証明することができる.他の問題をSATに変換して解く場合,式のサイズを小さくすることが効率の上昇に継ると考えられているが,本結果は,ある程度の冗長度を含ませることも重要である場合があることを示唆している.
|
Research Products
(6 results)
-
[Publications] Iwama, K.: "A canonical form of vector machines" Information and Computation. (to appear).
-
[Publications] Iwama, K.: "Better approximations of non-Hamiltonian graphs" Discrete Applied Mathematics. 81. 239-261 (1998)
-
[Publications] Iwama, K.: "Complexity of Finding Short Resolution Proofs" Proc.22nd Symposium on Mathematical Foundation of Computer Sceince(MFCS'97). LNCS1295. 309-318 (1997)
-
[Publications] Iwama, K.: "Three-dimensional mashes are less powerful than two-dimesional ones in oblivious routing" Proc.Fifth Europian Symposium on Algorithms(ESA'97). LNCS1284. 284-295 (1997)
-
[Publications] Iwama, K.: "Local search algorithms for partial MAXSAT" Proc.AAAI' 97. 263-268 (1997)
-
[Publications] Iwama, K.: "Random benchmark circuits with controlled attributes" Proc.European Design & Test Conference and Exhibition(ED&TC' 97). 90-97 (1997)
