📄 中文摘要
经典规划问题通常使用提升的第一阶表示来定义，这种表示方式具有紧凑性和普遍性。大多数规划器通过对这些表示进行基础化来简化推理，但这可能导致规模呈指数级膨胀。最近的研究直接在提升层面上操作，以避免完全基础化。提出了一种介于完全提升和完全基础化之间的中间方法，通过引入三种SAT编码，保持动作的提升性，同时部分基础化谓词。与之前的SAT编码相比，该方法在计划长度上呈线性扩展，显著提高了对较长计划的性能。实证结果表明，最佳编码在长度最优规划中超越了当前的最先进技术。
当有和没有基础不良时——一种部分基础编码的规划到SAT
📄 English Summary
When both Grounding and not Grounding are Bad -- A Partially Grounded Encoding of Planning into SAT (Extended Version)
Classical planning problems are typically defined using lifted first-order representations, which provide compactness and generality. Most planners simplify reasoning by grounding these representations, but this can lead to exponential size blowup. Recent approaches operate directly at the lifted level to avoid full grounding. A middle ground is introduced through three SAT encodings that maintain lifted actions while partially grounding predicates. Unlike previous SAT encodings that scale quadratically with plan length, this approach scales linearly, resulting in improved performance on longer plans. Empirical results demonstrate that the best encoding outperforms the state of the art in length-optimal planning.