STRIPS 规划模型的同构与嵌入

确定两个 STRIPS 规划实例是否同构是规划实例之间最简单的比较形式，也是寻找规划实例 $P$ 与另一个实例子集 $P_0$ 同构问题的特例。此类映射的一个应用是从包含 $P_0$ 所有解的编译形式中，高效地生成包含 $P$ 所有解的编译形式。我们还引入了从实例 $P$ 嵌入到另一个实例 $P_0$ 的概念，这允许我们推断出如果 $P$ 无解，则 $P_0$ 也无解。本文研究了这些问题的复杂度。我们证明，第一个问题是 GI-complete，因此在理论上可在准多项式时间内求解。尽管我们证明其余问题为 NP-complete，我们提出了一种在可能的情况下构建同构的算法。我们报告了在基准问题上的大量实验结果，这些结果明确地表明，在预处理中应用约束传播可大大提高 SAT 求解器的效率。