The Research On Several Issues Of Automated Reasoning And Artificial Intelligent Planning

Automated reasoning and artificial intelligent planning have always been the heart and most challenge fields in the research of artificial intelligence, and have always been the most successful fields as well. Since 1990, they have played important roles in the research of software generation and verification, protocol verification, hardware verification and robot planning.Our work mainly involves:(1) In recent years we have viewed tremendous improvements in the field of Propositional satisfiability (SAT). Many NP-complete problems from a variety of domains, such as classic planning problems, have been compiled into SAT instances, and solved effectively by SAT solvers. On the other hand, the problem of counting the number of models of a prepositional formula is an important extension of satisfiability testing. Recent research has also shown that model counting corresponds to numerous #P-complete problems such as performing inference in Bayesian networks, conformant probabilistic planning.Resolution principle is the rule of inference at the basis of most procedures for both SAT and #SAT, though a number of techniques, such as clause learning, variable selection, can be integrated to improve performance. In this paper, we propose a new method for (weighted) model counting. This work is motivated by Lin Hai's work, which used extension rule to solve SAT problems. The key idea of extension rule is to use the inverse of resolution and inclusion-exclusion principle to circumvent the problem of space complexity. This paper explores what happens if we use extension rule for (weighted) model counting. We propose four distinct algorithms for (weighted) model counting: model counting using extension rule (CER), model counting via knowledge compilation (KCCER), weighted model counting using extension rule (CWER), weighted model counting via knowledge compilation (KCCWER).In algorithm CER, we show that the extension rule based methods can be easily extended to count models. In algorithm KCCER, we prove that EPPCCL theory can solve #SAT problems in polynomial time. Therefore using knowledge compilation, a given clause set can be transformed into a form, in which model counting problems can be solved easily. We also showed in algorithm CWER and algorithm KCCWER that extension rules can be used in solving weighted model counting problems. We prove that all these alogrithms are sound and complete. Based on this idea, we have built a model counter: JLU-ERWMC. Experimental results have shown that this system outperform the most efficient model counters on some problems.(2) Possiblistic logic is especially useful for representation and reasoning under uncertainty when the given knowledge is inconsistent. It has been widely used in many fields such as belief revision, non-deteministic planning, and qualitative decision. In possiblistic logic, possibilistic resolution principle is the most basic inference rule. Extension rule is the complementary method of resolution. Here we introduce a generalization of extension in possibilistic, i.e. possibilistic extension rule. We introduce a novel framework for reasoning in possibilistic logic. Similar to classic logic, when the complementary factor is large, possibilistic extension rule is more efficient.Knowledge compilation is one of the most important problems in automated reasoning. By knowledge compilation, we can transform a given set of formulae into a form that can be deduced easier. After knowledge compilation, automated reasoning problems can be solved in polynomial time. We extend the concept of"tractable satisfiability"and"tractable entailment"in classic logic by introducing the concept of"tractable inconsistent degree computing"and"tractable optimal entailment". We prove that"tractable inconsistent degree computing"and"tractable optimal entailment"are the generalization of"tractable satisfiability"and"tractable entailment". Based on extension rule, we define the theory of EPPCCCL (Each Pair of Possibilistic Clauses Contains Complementary Literal). We prove that EPPCCCL is in the class of"tractable inconsistent degree computing"and"tractable optimal entailment". Thus EPPCCCL can be regarded as the target language for possibilistic knowledge compilation. We introduce how to compile a given possibilistic knowledge base into EPPCCCL and prove that this method is complete and sound.(3) Conformant planning is the task of generating plans when the initial state is partially known and the actions can have non-deterministic effects. While a classical plan must achieve the goal starting from a specific initial state, a conformant plan must achieve the goal regardless of uncertainty in the initial state and action effects. In recent literals, many researchers make the assumption that, in conformant planning domains, actions are all deterministic, and therefore all uncertainty lies in the initial situation. Even under this restriction, conformant planning is still computationally harder than classical planning yet, and this additional complexity cannot be reduced.We introduce a heuristic-based conformant planner, namely JLU-CD. Specifically, we show that conformant planning tasks can be transformed into a search problem in belief states space, each of whose elements is described in multi-valued domain formulation. We also show that causal graph and domain transition graph can be used to generate efficient heuristic for evaluating conformant planning. Unlike most"traditional"heuristic-based conformant planners, our planner computes heuristic in two phases. In the first phase, it estimates the cost of compiling uncertainty away. Interestingly, this process can be regarded as a process of solving Traveling Sales Problems (TSP). In the second phase, we estimate the cost of solving the resultant deterministic planning problems. Preliminary results have shown that our planner is competitive to other heuristic conformant planners.In this paper, we extend extension rule methods to solve #SAT problems. We also show extension rule can be generalized into possibilistic logic by introducing possibilistic extension rule. We introduce the framework for reasoning and knowledge compilation in possibilistic logic using possibilistic logic. We also build a multi-valued based conformant planner, which is competitive to other heuristic conformant planners. On the whole, the achievements of this thesis provides effective methods and means for the research on the automated reasoning and artificial intelligence planning methods.