基于时序归结的 LTL 不可满足核提取

不可满足核（Unsatisfiable Cores, UCs）是声明式场景中一种成熟的调试手段。然而，针对线性时序逻辑（LTL）进行自动化 UC 提取的工具仍然很少。现有工具将 UC 计算为 LTL 公式顶层合取项集合的一个不可满足子集。在 SAT 等其他领域中，使用归结图提取 UC 是常见做法。本文针对基于时序归结的求解器 TRP++ 中实现的时序归结，构建并优化了归结图，并利用它们为命题 LTL 提取 UC。所得 UC 比现有工具得到的 UC 粒度更细，因为 UC 提取过程还会对顶层合取项进行化简，而非将其视为原子实体。例如，给定一个形如 $\phi \equiv ({\bf G} \psi) \wedge {\bf F} \psi'$ 的不可满足 LTL 公式，现有工具无论 $\psi$ 和 $\psi'$ 的复杂度如何，都会将 $\phi$ 整体作为 UC 返回，而本文提出的方法会继续移除 $\psi$ 和 $\psi'$ 内部与不可满足性无关的部分。我们的方法还能识别出在不可满足性证明中不发生交互的命题出现组。我们在 TRP++ 中实现了该方法。实验评估表明，我们的方法 (i) 能够以可接受的开销提取出通常比输入公式显著更小的 UC，并且 (ii) 能产生比竞争工具粒度更细的 UC，同时在运行时间和内存使用方面至少保持竞争力。我们工具的源代码已公开。