Research On The Upper Bounds And The Phase Transformation Of The Automated Reasoning And The Planning

The automated reasoning and the planning are two important and difficult fields of the artificial intelligent. In 1971, Cook et al. have proved that the propositional satisfiability (SAT) is a NP-complete problem. In 1991, Chenoweth et al. have proved that the simple block problem in a close world is at least a NP-complete problem. If P≠NP, it means that these problems can't be solved in the polynomial time. In addition, recent SAT solvers have been able to solve SAT instances with hundreds of thousands variables. And the planners have been also able to solve the planning instances with more than one million states in ten seconds. The wide gap between the theory and the empirical data attracts more researchers to focus on the upper bounds and the phase transitions of the automated reasoning and the planning. Theoretical studies on the automated reasoning and the planning can understand problems essentially, reveal the solving rule of problems, and explain why these problems are solved difficultly. Moreover, these studies are crucial in determining the size of problems that can be solved. Take the model counting problem (#SAT) for example. Even a slight improvement from O(c~k) to O((c-ε)~k) may significantly increase the size of the #SAT problem being tractable. In addition, although the researches focusing on the upper bounds and the phase transitions can't proof whether P, NP, and PSPACE are equivalent, they can make us understand which problem is easy to solve and which problem is difficult to solve. This helps to design the algorithms according to the characteristics of the problems.Recently, the researches related to the minimum upper bound have been analyzed mainly regarding the number of variables as the parameter, such as the model counting problem (#SAT). So far all algorithms for solving #SAT have been analyzed only based on the number of variables. In fact, as we know, the time complexity is calculated based on the size of the instances, which depends not only on the number of variables, but also on the number of clauses. Therefore, it is significant to exploit the time complexity from the other point of view, i.e. the number of clauses. Furthermore, in the early stage the researches about the phase transitions are finished by the physicists. Since 2006 these work has been paid more attention by the computer scientists. However, only NP-complete problem is studied deeply among those researches relevant to this work. With regard to the automated reasoning and the planning, NP-complete problem is one of the simplest problems. There exists further up the polynomial hierarchy in problems, such as the conformant planning problem. Therefore, this thesis makes an in-depth study on the upper bounds and the phase transitions of the automated reasoning and the planning. The main parts of my work are as follows.(1) We exploit new upper bounds for #2-SAT using the number of clauses as the parameter. A new principle, i.e. the five-vertex principle, is developed to simplify formulae. This allows us to eliminate variables whose degree is 3, and therefore improves the efficiency of the algorithm. In addition, by transforming a formula into a constraint graph, we propose some detailed analyses between the adjacent variables in the constraint graph, which provides us theoretical foundations for choosing better variables to branch. By analyzing the algorithm, we obtain the worst-case upper bound O(1.1892~m) for #2-SAT, where m is the number of clauses.(2) We exploit new upper bounds for #3-SAT using the number of clauses as the parameter. By combining different branching selection methods, an algorithm MCDP based on Davis-Putnam-Logemann-Loveland (DPLL) for solving #3-SAT is presented. According to analyzing the algorithm, we obtain the worst-case upper bound O(1.8393~m) for #3-SAT, where m is the number of clauses in a formula. In order to increase the efficiency, we provide algorithm MC3 for solving #3-SAT. For the algorithm, we first simplify the 3-clause formulae into 2-clause formulae, then solve these 2-clasue formulae by the algorithm for #2-SAT. To demonstrate that this strategy is efficient, we give a deep analysis and obtain the worst-case upper bound O(1.4142~m) for #3-SAT, where m is the number of clauses in a formula.(3) We exploit new upper bounds for #SAT using the number of clauses as the parameter. An inference and analysis algorithm for solving #SAT problem based on extension rules is presented. We analyze the algorithm and prove an upper bound O(2~m) regarding the number of clauses as parameter, where m is the number of clauses in a formula. In addition, a #SAT solver based on the algorithm is designed, namely IAER. This solver incorporates the unit literal rule, the equality reduction rule, and the hyper-binary resolution rule in the preprocessing. And it also combines the component analysis technology for partitioning problems in the component analysis process. The experimental results show that IAER can solve #SAT problems efficiently, which validates the effect of these technologies in #SAT solving process.(4) We explore phase transitions of the EXPSPACE-complete problems, which mainly focus on the conformant planning problems. The research presents conformant PLAN-NONEXISTENCE algorithm, conformant PLAN-EXISTENCE algorithm and gives two bounds on the number of operators. If the number of operators isn't greater thanαub, then conformant PLAN-NONEXISTENCE algorithm can prove that all most conformant planning problems have no solutions. If the number of operators isn't lower thanαlb, conformant PLAN-EXISTENCE algorithm can prove that all most conformant planning problems have solutions. The results of the experiment show that there exists an experimental thresholdαc of density (the number of actions divide the number of propositions), which separates the region where almost all conformant planning problems have no solutions from the region where all problems have solutions.Above all, this thesis makes an in-depth study on the upper bounds and the phase transitions of the automated reasoning and the planning, which mainly focus on the #SAT problem and the conformant planning problem. The rigorous theoretical analyses about the algorithms for #SAT can not only reveal the essential nature of the problems, but also increase the size of the problem being tractable for even a slight improvement may increase the efficiency of the algorithms. The rigorous theoretical analyses about the transition point of the conformant planning problem can not only evaluate quantitatively the phase transition zone of the conformant planning problem, but also help to design the algorithms according to the characteristics of the problems. Therefore, the results of this paper are of great significance to the automated reasoning and the planning.