1997 Fiscal Year Final Research Report Summary
Computational Complexity of Automated Theorem Proving
| Project/Area Number |
08044158
|
|---|
| Research Category |
Grant-in-Aid for international Scientific Research
|
| Allocation Type | Single-year Grants |
|---|
| Section | Joint Research . |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYOTO UNIVERSITY (1997)
Kyushu University (1996) |
|---|
Principal Investigator |
IWAMA Kazuo Graduate School of Engineering, Professor, 工学研究科, 教授 (50131272)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
PAUL Purdom Indiana University, CS,Professor, 計算機科学科, 教授
RUSSELL Impagliazzo University of California San Diego, CS & E,Associate Professor, 計算機科学科, 助教授
SAKURAI Kouichi Kyushu University, CS & CE,Associate Professor, 大学院・システム情報科学研究科, 助教授 (60264066)
TONIANN Pitassi University of Arizona, CS,Assistant Professor, 計算機科学科, 助教授
|
|---|
| Project Period (FY) |
1996 – 1997
|
| Keywords | theorem proving / Resolution / computational complexity |
|---|
| 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 NP-hard, 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.
|
