Research On Intelligent Planning Methods Based On Automated Reasoning Techniques

Intelligent planning is one of the most important areas of artificial intelligence researches, and also a multi-field cross-discipline covering knowledge representation, automated reasoning, non-monotonic logic, human-computer interaction, cognitive science, etc. Intelligent planning research originated from automated reasoning and knowledge representation. It could usually be solved by logical deduction methods until the 90 years of 20th century and mainly focused on the use of various reasoning techniques of classical logics. Blum and Furst proposed a novel planner based on planning graph in 1996, called Graphplan, which excellently resolved the exponential space explosion problem during the knowledge representation processing excellently. It also made the relevant researchers pay attention to intelligent planning research area from then on.Intelligent planning is generally defined as"to draw up an action sequences comprehensively to achieve the predefined goal state, by understanding and analyzing the surrounding environments, and reasoning on a number of alternative actions and the resource constraints provided".Along with various kinds of new techniques for intelligent planning have been proposed one after the other, the different kinds of planning methods could be used to deal with the abstract and complex issues of real-world better. Currently, existing planning methods can be divided into two categories: translation based intelligent planning methods and state-space heuristic searching based intelligent planning methods.Translation based intelligent planning method, directly or indirectly translates a given planning problem into a number of classical problems, such as propositional satisfiability problems, model checking problems, constraint satisfiability problems, linear programming problems, non-classical logic theorem proving problems, etc. This method could indirectly revolves the original planning problem by efficiently solving of the translated target problems. Because of the quasi first-order predicate logic representation of planning problems, logical deduction and reasoning techniques have been used in most translation based planning methods to some extent.Intelligent planning method based on automated reasoning techniques (or automated reasoning techniques based intelligent planning method) is a translation based planning method, which can be interpreted in a narrow sense as: Depending on the potential semantics of planning problem, it translations a given planning problem into a number of theorem proving problems of a certain logic representation, then calls the corresponding logic proving systems to solve them, and at last decodes the solution of translated target problems to a valid plan of original planning problem.The main objective of this kind of planning method is to design the knowledge representations of planning problem more formally and specifically, and theoretically guarantee the planning method could be built on the basis of formal systems with soundness and completeness.In this paper, it mainly focuses on intelligent planning methods based on automated reasoning techniques: propositional logic based encoding methods and planning methods for solving classical planning problems, modal logic based encoding methods and planning methods for solving Conformant planning. The main contributions include:(1) It summarizes the intelligent planning methods based on automated reasoning techniques, including research background, the concepts related to encoding and reasoning, and a variety of intelligent planning methods based on automated reasoning techniques. Firstly, it introduces the foundation of encoding, including the definitions, representations, characteristics and conclusions; Secondly, it introduces the related reasoning techniques, including deductions and decisions; Finally, it introduces the detailed planning methods based on propositional satisfiability, Conformant planning methods based on modal logic, the planning methods based on non-monotonic logic, the Flexible planning method based on fuzzy description logic, the planning methods based on constraint satisfaction problem, the planning method based on binary decision diagram, the planning method based on multi-valued variables, etc. It highlights the planning methods based on propositional satisfiability, including research background, framework, knowledge representations, encoding methods, reasoning abilities, deciding methods, planners, etc.(2) It proposes the reducing theories and propositional logic encoding methods based on compacted theories. Firstly, it proposes the selection strategies of overlapped axioms and the deletion strategies of redundant axioms via analyzing the Graphplan based encoding, and also proposes the selection strategies of overlapped axioms via analyzing the state based encoding. After reducing processing, the size of target encodings can be efficiently decreased. It justifies the soundness and completeness of proposed strategies theoretically and analyzes the reducing results; Secondly, it proposes the preprocessing method for goal states during encoding solving process, and it also proposes a new encoding method, called PMA based encoding method, by reducing mutex axioms of actions based on Graphplan based encoding; Thirdly, it proposes a new encoding method, called FA based encoding method, by adding frame axioms; Finally, it justifies the soundness and completeness of them, respectively, and tests them using benchmarks adopted by International Planning Competition. By comparing the evaluation parameters, it analyzes the advantages and disadvantages of different encoding methods for different kinds of planning problems.(3) Based on action based encoding, it proposes a new planning encoding method by reducing action variables, called proposition based encoding method, which only depends on state variables. It justifies the soundness and completeness of the corresponding encoding method, and also analyzes the distinctions between it and existed encoding methods. Finally, it tests proposition based encoding using benchmarks adopted by International Planning Competition. By comparing the evaluation parameters, it analyzes the advantages and disadvantages of two extreme encoding methods for different kinds of planning problems.(4) It briefly introduces the Conformant planning methods, relevant planning methods based on modal logic, planners and knowledge representations, and proposes Conformant planning methods based on modal logic. Firstly, it introduces the existed knowledge representations based on modal logic; Secondly, it determines that Conformant planning is equivalent to automated reasoning of D proving system, by analyzing the transformations between relevant states, knowledge representations of propositions and formulae in relevant states, semantic interpretations of possible world semantics; Thirdly, these methods translate a Conformant planning problem into a series of automated reasoning problems based on modal logic axiomatic system D using the corresponding modal semantics of the planning problems. The initial belief state and operations are translated to the axioms and rules of modal logic, and the goal is translated to the theorem to be proved. It ensures that the theorem proving processing of corresponding axiomatic system is equivalent to the planning processing of original problem. Finally, it illustrates the soundness of these methods.(5) It proposes compositional planning methods based on modal logic by analyzing the side effects of undeterministic actions in multi-possible states in Conformant planning. Firstly, it analyzes a simple reasoning of Conformant planning method based on automated reasoning, and proposes some counter-examples to reveal its reasoning capabilities and deficiencies; Secondly, it defines the corresponding concepts of modal optimal compositional plan, modal compactness plan and modal planning possible state to describe Conformant plan obtained by combining classical plans; Thirdly, it proposes two Conformant compositional planning method based on modal logic: a plain compositional planning method and a compositional planning method with constraints; Finally, it illustrates the soundness of these methods. These methods implement the disjunctive reasoning and necessity reasoning from a logical encoding of view, eliminates the side effects of undeterministic actions in multi-possible states, improves the processing capability of Conformant planning method based on modal logics, can be used to solve Conformant planning problems with multi-states and disjunctive actions.In addition, this paper also analyzes the difficulties encountered during researching period, and the possible further research directions. In summary, the theoretical results of this paper should lay the foundations for the formal representation and general processing in intelligent planning methods based on automated reasoning techniques, and also further improve the processing capabilities and solving efficiencies of intelligent planners, so it is possible that they could be used to solve widespread, large-scale, intractable, complex problems in real world requiring a certain intelligence. So, they have a certain theoretical value and significance.