Computational Complexity of Automated Theorem Proving

点击翻译按钮获取中文摘要

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.