论文研究规划问题编码成SAT问题研究.pdf

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