Project/Area Number  08044158 
Research Category 
GrantinAid for International Scientific Research.

Section  Joint Research . 
Research Field 
計算機科学

Research Institution  KYOTO UNIVERSITY 
Principal Investigator 
IWAMA Kazuo Graduate School of Engineering, Professor, 工学研究科, 教授 (50131272)

CoInvestigator(Kenkyūbuntansha) 
PAUL Purdom Indiana University, CS,Professor, 計算機科学科, 教授
RUSSELL Impa カリフォルニア大学(サンジエゴ校), 計算機科学科, 助教授
SAKURAI Kouichi Kyushu University, CS & CE,Associate Professor, 大学院・システム情報科学研究科, 助教授 (60264066)
TONIANN Pita アリゾナ大学, 計算機科学科, 助教授
IMPAGLIAZZO カリフォルニア大学(サンジエゴ校), 計算機科学科, 助教授
PITASSI Toni アリゾナ大学, 計算機科学科, 助教授
RUSSELL Impagliazzo University of California San Diego, CS & E,Associate Professor
TONIANN Pitassi University of Arizona, CS,Assistant Professor

Project Fiscal Year 
1996 – 1997

Project Status 
Completed(Fiscal Year 1997)

Budget Amount *help 
¥2,200,000 (Direct Cost : ¥2,200,000)
Fiscal Year 1997 : ¥1,100,000 (Direct Cost : ¥1,100,000)
Fiscal Year 1996 : ¥1,100,000 (Direct Cost : ¥1,100,000)

Keywords  theorem proving / Resolution / computational complexity / 定理証明 / 導出原理 / 計算複雑さ / 定理の自動証明 / NP完全性 / SAT 
Research Abstract 
Automated theorem proving system is one of the most popular topics of AI field and has been discussed by many researchers. However, there is no perspective of making it into practical use because of the lack of fundamental analysis on it. In this research work, we discussed the intractability of Resolution, a theorem proving system of tautology. We obtained the following results : (1) A lot of effort has been done for the problem of finding Resolution proofs and fast algorithms are developed recently. We analyzed this problem in terms of optimization, i.e., the problem of finding shortest Resolution proofs. We showed that the problem of finding a proof of length less than S+O(n^d) is NPhard, where n is the number of variables, S is the length of the shortest proof, and d is an arbitrary constant. (2) We discussed the relation between Resolution and Backtracking method, an algorithm for CNF Satisfiability problem (SAT). We showed that a search tree of Backtracking can be obtained from Resolution proof without increasing the size of the tree, and vice versa. (3) We found a set of CNF formulas such that we can reduce the length of the proof by adding redundancy. Let NH be the set of formulas obtained by translating some graph problem into SAT.NH needs exponential length of Resolution proof. However, if we add small number of clauses to formulas in NH,we can prove NH in polynomial number of steps. In some occasions, we solve hard combinatorial problems translating into SAT.In this case, it seems reasonable to translate the original problem into short formulas. However, our result shows that there are some occasions in which redundancy plays an important role.
