SAT-Based Parallel Planning Using a Split Representation of Actions
SAT-Based Parallel Planning Using a Split Representation of Actions
复制标题
使用动作的分割表示的基于 SAT 的并行规划
DOI：
10.1609/icaps.v19i1.13368
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
A. Sattar
中科院分区：
文献类型：
--
作者：
Nathan Robinson;Charles Gretton;D. Pham;A. Sattar
规划的基础上命题SAT（isfiability）是一个强大的方法来计算步骤最优计划给定的并行执行语义。在这种情况下：（i）解决方案计划在所需的计划步骤的数量上必须是最小的，以及（ii）在计划步骤处可以并行地立即执行不冲突的动作。潜在的SAT为基础的方法是调用一个决策程序的SAT编码的有界版本的问题。现有方法的一个基本限制是这些编码的大小。这个问题源于使用动作的直接表示-即每个动作在编码中都有相应的变量。在规划中的一个长期目标是通过开发一个更紧凑的分裂-也称为提升-在并行步骤优化问题的SAT编码中表示动作来减轻这种限制。本文描述了这样一种表示。特别地，每个动作和动作的每个并行执行被唯一地表示为变量的合取。在这里，每个变量都是从动作的前置条件和后置条件中派生出来的。由于多个动作共享条件，我们对规划约束的编码是分解的，并且相对紧凑。我们发现实验，我们的编码产生了一个更有效的和可扩展的规划程序在一个大的规划基准集的最先进的。
Planning based on propositional SAT(isfiability) is a powerful approach to computing step-optimal plans given a parallel execution semantics. In this setting: (i) a solution plan must be minimal in the number of plan steps required, and (ii) non-conflicting actions can be executed instantaneously in parallel at a plan step. Underlying SAT-based approaches is the invocation of a decision procedure on a SAT encoding of a bounded version of the problem. A fundamental limitation of existing approaches is the size of these encodings. This problem stems from the use of a direct representation of actions — i.e. each action has a corresponding variable in the encoding. A longtime goal in planning has been to mitigate this limitation by developing a more compact split — also termed lifted — representation of actions in SAT encodings of parallel step-optimal problems. This paper describes such a representation. In particular, each action and each parallel execution of actions is represented uniquely as a conjunct of variables. Here, each variable is derived from action pre and post-conditions. Because multiple actions share conditions, our encoding of the planning constraints is factored and relatively compact. We find experimentally that our encoding yields a much more efficient and scalable planning procedure over the state-of-the-art in a large set of planning benchmarks.