在本文中，我们提出了一种基于符号模式规划（SPP）的数值规划程序。给定数值规划问题 $ ext{Π}$，模式 $ ext{⟨p⟩}$ 是一系列动作，用于定义从起始状态 $ ext{S}$ 可执行的 $ ext{⟨p⟩}$ 子序列的公式。Cardellini、Giunchiglia 和 Maratea（2024a）遵循规划为可满足性的方法，在每一步 $ ext{n} ext{≥} 0$ 中定义公式 $ ext{Π}^{ ext{⟨p⟩}}_n$，其中 $(i)$ 模式 $ ext{⟨p⟩}$ 仅在 $ ext{n}=0$ 时在 $ ext{Π}$ 的初始状态 $ ext{I}$ 中计算，并在每一步 $ ext{n}$ 中利用， $(ii)$ 起始状态 $ ext{S}$ 设置为 $ ext{I}$， $(iii)$ 目标集合 $ ext{G}$ 要求在通过 $ ext{⟨p⟩}$ 子序列连接 $ ext{n}$ 次后可达的最后状态中成立。该程序从 $ ext{n}=0$ 开始，直到 $ ext{Π}^{ ext{⟨p⟩}}_n$ 可满足为止，否则通过增量增加 $ ext{n}$ 继续进行。在本文中，可能在每一步中， $(i)$ 我们在 $ ext{I}$ 中符号搜索一个可达的中间状态 $ ext{P}$，该状态更接近目标状态， $(ii)$ 动态重新计算将用于下一步的模式 $ ext{⟨p⟩}_h$， $(iii)$ 精炼用于到达 $ ext{P}$ 的模式 $ ext{⟨p⟩}_g$， $(iv)$ 从状态 $ ext{S}$ 开始新搜索，$ ext{S}$ 可以是初始状态 $ ext{I}$ 或最后计算的中间状态 $ ext{P}$，利用计算出的模式 $ ext{⟨p⟩}_g$ 和 $ ext{⟨p⟩}_h$ 来定义在搜索中使用的模式 $ ext{⟨p⟩}$。特别地，在每一步中，我们定义公式 $ ext{Π}^{ ext{⟨p⟩}}_{S,P}$，编码从起始状态 $ ext{S}$ 可达的、比 $ ext{P}$ 更接近目标状态的状态 $ ext{P}'$ 的存在。我们提出了产生这些公式的不同技术，每种技术对应于探索搜索空间的不同策略。我们证明了它们的正确性和完整性，后者在某些条件下成立。
博主点评： 本文通过引入符号模式规划的概念，为数值规划问题提供了一种新的解决方案。通过动态搜索和模式重计算的结合，显著提高了搜索效率和可达性，为后续的研究提供了重要的理论基础。该方法在具体实现中可能需要处理复杂性和计算资源的平衡问题。