《Journal of Logical and Algebraic Methods in Programming》：Efficient SMT formulations for classical planning
编辑推荐：
人工智能规划（AI planning）是为一个声明式描述的系统寻找动作序列以达成某个目标，同时（可选地）优化某些度量指标的任务。在其经典版本中，初始状态完全已知，动作具有确定性的已知效果。除了概念上的简洁性，经典规划对于满足性规划和最优规划都是PSPACE完全
人工智能规划（AI planning）是为一个声明式描述的系统寻找动作序列以达成某个目标，同时（可选地）优化某些度量指标的任务。在其经典版本中，初始状态完全已知，动作具有确定性的已知效果。除了概念上的简洁性，经典规划对于满足性规划和最优规划都是PSPACE完全的（PSPACE-complete），因此存在大量启发式规划器，以不同方式应对问题的固有复杂性。尽管如此，在许多情况下，基于SAT（Boolean satisfiability，布尔可满足性）的精确方法与启发式方法在经典规划中具有竞争力。已有几种声明式语言被提出用于经典规划，例如STRIPS（Stanford Research Institute Problem Solver，斯坦福研究所问题求解器）和PDDL（Planning Domain Definition Language，规划域定义语言），其中PDDL是大多数规划器至少在一定程度上支持的事实标准。PDDL公式包含一阶公式，通常需要实例化（grounding）以求解规划问题，无论是采用启发式方法还是精确方法，这有时会导致公式膨胀，使得实例变得难以处理。基于此，本研究（研究人员）提出了一项关于将PDDL公式转化为SMT（Satisfiability Modulo Theories，可满足性模理论）中提升表示（lifted representations）的研究，旨在为经典规划获得更紧凑且同时高效的公式。研究人员表明，在难以实例化（hard-to-ground）的实例上，SMT公式通常优于基于SAT的公式。
自动规划是人工智能领域的一个活跃研究方向，其任务是寻找从已知初始状态到目标状态的动作序列。经典规划问题由于PSPACE完全性而具有高复杂度，启发式方法虽广泛存在，但基于SAT的精确方法在部分场景中具有竞争力。PDDL作为标准建模语言，其公式通常需要实例化处理，导致公式爆炸，阻碍了问题求解。针对这一挑战，研究人员在发表于《Journal of Logical and Algebraic Methods in Programming》的论文中，探索了将PDDL转化为SMT提升表示的方法，以兼顾紧凑性与求解效率。研究结果表明，基于SMT的提升编码在难以实例化的实例上优于传统SAT编码，为处理这类问题开辟了新途径。
研究人员首先回顾了经典规划和PDDL的基础概念，并介绍了基于SAT的规划编码及其限制。在此基础上，提出了三种基于SMT的一阶逻辑编码：全量化编码（fully quantified FOL）、部分量化编码（partially quantified FOL）和无量词提升编码（quantifier-free lifted FOL）。全量化编码虽紧凑但求解性能差；部分量化编码仅对时间进行量化，参数部分实例化；无量词提升编码保留动作的模式参数，但框架公理仍需实例化。为提升效率，研究人员利用Fast Downward预处理器的可达性分析，提出了两种域约简策略：约束算子（constrained operators）和半约束算子（semi-constrained operators），分别通过限制动作实例和参数域来缩减编码规模。实验采用国际规划竞赛（IPC）的STRIPS域基准测试，并包含部分难实例化域，使用Z3求解器（版本4.15.4）进行测试，超时时间设为1小时，内存限制为16 GB。
**5. 实证评估**
通过比较不同编码的求解性能，得出以下结论：
- **SAT与SAT-FD比较**：SAT-FD通过过滤无关实例化显著优于朴素SAT编码，在多数实例上表现更好。
- **SAT-FD与SMT比较**：SMT编码整体优于SAT-FD，尤其在减少超时和内存溢出方面表现突出，这是本研究的主要贡献。
- **SMT与SMT-FD-C比较**：基于约束算子的SMT-FD-C编码并未提升性能，甚至有所下降。
- **SMT与SMT-FD-SC比较**：半约束算子SMT-FD-SC编码普遍优于SMT，减少了超时次数，缩短了求解时间。
- **SMT-FD-SC与SAT-FD比较**：SMT-FD-SC持续优于SAT-FD，进一步验证了SMT方法的有效性。
- **SMT-FD-SC与Madagascar比较**：在顺序模式下，SMT-FD-SC明显优于基于SAT的规划器Madagascar（MS）。
- **与LiSAT、Q-Planner和Fast Downward比较**：SMT-FD-SC在求解实例数上不及LiSAT和Fast Downward，但优于Q-Planner，且是唯一未出现内存溢出的方法。
**总结讨论**
研究人员指出，SMT提供了表达性与效率的良好折中。全量化编码表现不佳，但无量词提升编码在多数实例上优于纯SAT编码，即使实例化限制在相关原子和算子上。SMT的优势不仅体现在内存需求上，也体现在求解时间上。此外，简单的SMT编码（SMT-FD-SC）与基于SAT的规划器Madagascar的序列版本相比具有竞争力，并在许多难实例化实例上胜出。本研究首次系统探索了未解释函数在规划中实现紧凑公式的应用，为处理难实例化规划问题开辟了新途径。未来工作将把相关思想扩展到并行规划场景。
**结论部分翻译**
研究人员提出了几种紧凑的基于SMT的经典规划编码，表明提升的SMT编码在难以实例化的问题上优于基于SAT的编码。SMT在内存和求解时间上均具有优势，且与基于SAT的规划器Madagascar的序列版本相比具有竞争力，并在许多难实例化实例上胜出。
