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

摘要： 智能规划问题是一个NP-hard的问题。近年来，由于在可满足问题（SAT）研究领域取得了较大进展，出现了一大批快速的能达到工业级应用的SAT solver求解器的出现，这使得运用可满足技术来求解规划问题的方法越来越得到智能规划研究者们的重视。用可满足技术求解规划问题的首要任务是必须将规划问题“翻译”成可满足问题。讨论了如何将规划问题编码成命题可满足问题的一般技术，并对“直接编码”和“基于规划图的编码”两种编码技术进行了比较，指出了两种编码技术各自的优缺点。在此基础上，深入地分析了各种不同的编码方案之间的异同点以及它们各自的优缺点。最后，指出了用SAT技术求解规划问题中存在的一些问题以及相关改进方法。

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