关键词: 智能规划, 规划图, 可满足（SAT）问题, 编码方案

Abstract: Intelligent planning is a NP-hard problem，and using SAT technology to solve the planning is an important research direction.Recently，great progress has been made on SAT technology，many fast SAT solver has appeared，which lead the planning method based on SAT technology to be a competitive method and attract many researcher’s focus.The first problem to be solved when using SAT to solve planning problem is to translate the planning problem into a SAT problem.This paper discusses the general technology on encoding the planning problem into SAT problem，and gives some comparisons between directly encoding method and encoding method based on planning graph.Finally this paper points out some problems exist in current planning technology based on SAT and gives some possible method on how to improve the current planner based on SAT technology.

Key words: intelligent planning, planning graph, SAT problem, encoding schema