单位二变量不等式（UTVPI）的插值生成

### 单位二变量不等式（UTVPI）的插值生成 #### 1. 背景与动机 在形式验证领域，计算SMT（Satisfiability Modulo Theory）中的Craig插值项的问题近年来备受关注。给定两个公式A和B，若A ∧ B不一致，那么Craig插值项I需满足：A蕴含I，I ∧ B不一致，且I中的所有未解释符号同时出现在A和B中。插值在形式验证中是一个重要工具，例如在基于反例引导的抽象细化（CEGAR）的软件模型检查中，会计算合适理论中无量词公式的插值项，以自动细化抽象，排除虚假反例。 近年来，针对一些感兴趣的理论，如等式和未解释函数（EUF）、有理数上的线性算术（LA(Q)）及其组合，已经提出了高效的插值生成算法和工具。然而，在许多应用中，有理数域往往不足以精确表示变量，整数域能更精确地表示变量。但计算整数上的线性算术（LA(Z)）的插值项比LA(Q)面临更多问题，目前还没有已知的高效算法，已知的基于量词消除的算法通常代价高昂，还需要引入可除性谓词。因此，研究LA(Z)的片段的插值是很有意义的。 单位二变量不等式（UTVPI）理论是LA(Z)的一个非常有用的片段。在UTVPI中，公式是形如(0 ≤ ax1 + bx2 + k)的原子的布尔组合，其中xi是整数变量，k是整数常量，a, b ∈ {-1, 0, 1}。UTVPI推广了著名的差分逻辑（DL(Z)），并且是LA(Z)中具有多项式决策过程的最具表达力的片段之一。UTVPI还能自然地表达许多硬件和软件验证问题中的查询。 #### 2. 相关概念 - **SMT（可满足性模理论）**：我们在标准一阶逻辑的框架下，考虑判定无量词公式相对于背景理论T的可满足性问题，记为SMT(T)。用φ |=T ψ表示公式ψ是φ在理论T中的逻辑结果。我们还假设公式是合取范式（CNF）。T - 求解器是用于判定T中文字合取的一致性的过程。如果S是T中的文字集合，T - 冲突集是S的一个不一致子集η，¬η是T - 引理。对于一组子句S和一个子句C，分辨率证明是一个有向无环图P，满足特定条件。解决SMT(T)问题的标准技术是将基于DPLL的SAT求解器和T - 求解器以懒惰的方式集成。 - **SMT中的插值**：对于背景理论T的SMT(T)问题，给定公式对(A, B)，若A ∧ B |=T ⊥，Craig插值项I需满足：A |=T I，I ∧ B是T - 不一致的，且I中的所有未解释符号同时出现在A和B中。插值项的生成基于A ∧ B的不可满足性的分辨率证明，具体算法如下： 1. 生成A ∧ B的不可满足性证明P。 2. 对于P中出现的每个T - 引理¬η，生成(η \ B, η ↓B)的插值项I¬η。 3. 对于P中的每个输入子句C，若C ∈ A，将IC设置为C ↓B；若C ∈ B，将IC设置为⊤。 4. 对于P中通过分辨率从C1 = p ∨ φ1和C2 = ¬p ∨ φ2得到的每个内部节点C，若p不在B中，将IC设置为IC1 ∨ IC2；否则，将IC设置为IC1 ∧ IC2。 5. 输出I⊥作为(A, B)的插值项。 - **差分逻辑的基于图的插值**：差分逻辑（DL）是线性算术理论的一个片段，其中所有原子都是形如(0 ≤ y