Even under polynomial restrictions on plan length, conformant planning remains a very hard computational problem as plan verification itself can take exponential time. This heavy price cannot be avoided in general although in many cases conformant plans are verifiable efficiently by means of simple forms of disjunctive inference. This raises the question of whether it is possible to identify and use such forms of inference for developing an efficient but incomplete planner capable of solving non-trivial problems quickly. In this work, we show that this is possible by mapping conformant into classical problems that are then solved by an off-the-shelf classical planner. The formulation is sound as the classical plans obtained are all conformant, but it is incomplete as the inverse relation does not always hold. The translation accommodates 'reasoning by cases' by means of an 'split-protect-and-merge' strategy; namely, atoms L/X_i that represent conditional beliefs 'if X_i then L' are introduced in the classical encoding, that are combined by suitable actions to yield the literal L when the disjunction X_1 an∨ … ∨ X_n holds and certain invariants in the plan are verified. Empirical results over a wide variety of problems illustrate the power of the approach..
展开▼
机译：即使在计划长度的多项式限制下，一致的计划仍然是一个非常棘手的计算问题，因为计划验证本身会花费指数时间。尽管在许多情况下可以通过简单形式的析构推理来有效验证符合计划，但通常无法避免此沉重的代价。这就提出了一个问题，即是否有可能识别和使用这种形式的推理来开发能够快速解决非平凡问题的有效但不完整的计划者。在这项工作中，我们证明了通过将符合者映射到经典问题中，然后由现成的经典计划者解决这些问题是可能的。该表述是合理的，因为所获得的经典计划都是一致的，但是由于逆关系并不总是成立，因此表述是不完整的。该翻译通过“拆分保护并合并”策略来适应“案例推理”。就是说，在经典编码中引入了表示条件信念'if X_i then L'的原子L / X_i，这些原子通过适当的动作组合起来，从而在分离X_1 an…∨X_n成立并且计划中有某些不变量时产生文字L经过验证。对各种问题的实证结果说明了该方法的强大功能。
展开▼
