数组理论 (二)

数组理论延迟编码过程

1. 基于DPLL(\(T\))的增量编码

数组理论 (一)说明了一种通过规约程序来实现将数组理论编码成带有索引下标和元素的理论. 本质上, 它是通过添加读写覆盖规则和扩展性规则的实例来实现的.实际上,算法生成的大多数实例都是不必要的, 也就增加了判定问题的计算成本. 所以要讨论一种新的程序或者算法, 该算法增量的生成读写覆盖和扩展性规则的实例. 设计该算法是为了能够集成到 DPLL(\(T\)) 程序中去. 它使用未解释函数将数组公式延迟编码为等式逻辑. 该算法假定索引理论是无量词的, 但是确实允许数组之间的相等性.

预处理

我们在算法主要阶段之前执行预处理步骤. 预处理步骤详尽地实例化了读覆盖写规则的前半部分, 比如说, 对于公式中存在的所有的表达式 \(a\{i\leftarrow e\}\), 添加相应的约束 \[ a\{i\leftarrow e\}[i]= e. \] 因此, 这就产生了线性数量的约束. 读覆盖写公理的第二种情况和扩展性规则将逐步实施.

在介绍增量编码之前, 简要地对DPLL(\(T\)) 的基本原则进行说明. 在 DPPL(\(T\)) 中, 命题 SAT 求解器用于获取公式中理论原子的(可能是部分)布尔赋值. 该赋值被传递给理论求解器, 该理论求解器确定该赋值是否为 \(T-consistent\). 理论求解器可以将添加的命题约束传递回 SAT 求解器, 以实现理论传播和理论学习. 这些约束将添加到由 SAT 求解器维护的子句数据库中. 然后, 该过程将迭代进行, 要么确定公式为 UNSAT, 要么生成新的(可能是部分的)布尔赋值.

2. 读覆盖写公理的延迟实例化

如下算法将一个数组公式的文字(也就是数组理论的原子)的集合作为输入. 文字的合取式记为 \(\hat{Th}\). 如果 \(\hat{Th}\) 是一致性的(为真), 算法返回\(\rm TRUE\); 否则返回一个在该数组理论下为真的公式 \(t\), 并且禁用之前的赋值 \(\hat{Th}\). 公式 \(t\) 初始化为 \(\rm TRUE\), 并且随着算法的执行会增强公式的正确性.

\[ \begin{aligned} &\mathbf{Algorithm\ 1:}\ \text{ARRAY-ENCODING-PROCEDURE}\\ &\mathbf{Input:}\quad\quad \text{A conjunction of array literals } \hat{Th}\\ &\mathbf{Output:}\quad\; \text{TRUE, or a valid array formula } t\ \text{that blocks } \hat{Th}\\ \\ &1.\; t:=\text{TRUE};\\ &2.\; \text{Compute equivalence classes of terms in } \hat{Th};\\ &3.\; \text{Construct the weak equivalence graph } G\ \text{from } \hat{Th};\\ &4.\; \mathbf{for}\; a,b,i,j\; \text{such that } a[i]\;\text{and}\; b[j]\ \text{are terms in } \hat{Th}\; \mathbf{do}\\ &5.\;\quad\quad \mathbf{if}\; i\approx j\; \mathbf{then}\\ &6.\;\quad\quad\quad\; \mathbf{if}\ a[i]\not\approx b[j]\ \mathbf{then}\\ &7.\;\quad\quad\quad\quad\; \mathbf{for}\;\text{each simple path } p\in G\ \text{from } a\;\text{to } b\; \mathbf{do}\\ &8.\;\quad\quad\quad\quad\quad\; \mathbf{if}\; \text{each label } l\; \text{on } p\text{'s edges satisfies } l\neq i\;\mathbf{then}\\ &9.\;\quad\quad\quad\quad\quad\quad\; t:=t\wedge ((i=j\wedge Cond_i(p))\Longrightarrow a[i]=b[j]);\\ &10.\; \mathbf{return}\;t; \end{aligned} \]

算法1 第2行中 \(\hat{Th}\) 提到的等价类会被计算出来. 之前已经说过如何使用同余闭包算法计算等价类. 我们用 \(t_1\approx t_2\) 表示项 \(t_1\) 和 \(t_2\) 在同一个等价类中.

算法1 第3行构造了一个带有标记的无向图 \(G(V,E)\), 称作弱等价图(weak equivalence graph). 顶点集 \(V\) 对应 \(\hat{Th}\) 中的数组项. 边集是有可选的标记, 并添加如下:

1. 对于数组项之间的每个等式 \(a = b\), 在 \(a\) 和 \(b\) 之间添加一个未标记的边.
2. 对于每个数组项 \(a\) 和对于该项的更新 \(a\{i\leftarrow v\}\), 在其顶点之间添加标记为 \(i\) 的边.

以下用一个例子进行说明. 考虑如下公式 \[ \begin{align*} \hat{Th}&\doteq i\ne j \land i\ne k\land a\{j\leftarrow v\}=b \land a\{k\leftarrow w\}\\ &= c\land b[i]\ne c[i].\tag{2.1} \end{align*} \] \(\hat{Th}\) 对应的弱等价图为:

每当 \(G\) 中存在从 \(a\) 到 \(b\) 的路径时, 两个数组 \(a\) 和 \(b\) 称为弱等效项(weakly equivalent). 这意味着它们在所有数组元素上均相等, 除了可能在路径上更新的元素之外. 上例中的数组 \(a, b\) 和 \(c\) 都是弱等价的.

算法1 第4-9行生成了增强数组元素等价性的约束. 这与 \(\hat{Th}\) 中的任何一对数组元素项 \(a[i]\) 和 \(b[j]\) 有关. 根据等价类, 其中索引项 \(i\) 和 \(j\) 必须是相等的, 但是 \(a[i]\) 和 \(b[j]\) 不相等. 这个想法是确定数组 \(a\) 和 \(b\) 是否通过不使用索引 \(i\) 的数组更新链进行连接. 如果存在具有此属性的链, 那么 \(a[i]\) 肯定等于 \(b[j]\). 我们将使用弱等价图 \(G\) 检查这个链是否存在. 我们将考虑从 \(a\) 到 \(b\) 的所有路径 \(p\). 如果根据我们的等价类, 路径中的任何一条边标签的索引等于 \(i\), 那么就可以丢弃该路径. 否则, 我们就找到了所需的链, 并将 \[ (i=j \land Cond_i(p))\Longrightarrow a[i]=b[j] \] 作为约束条件加入到 \(t\) 中. 表达式 \(Cond_i(p)\) 是以下合取的约束:

1. 对于从 \(a\) 到 \(b\) 的未标记边, 添加约束 \(a=b\).
2. 对于添加了标记 \(k\) 的边, 添加约束 \(i\ne k\).

继续上面的例子, 我们有两个非平凡的等价类: \(\{a\{j\leftarrow v\}, b\}\) 和 \(\{a\{k\leftarrow w\}, c\}\). 因此, 项 \(b[i], c[i]\) 满足 \(b[i]\ne c[i]\), 而且它们的索引是大致相等的. 在图 \(G\) 上有一条从 \(b\) 到 \(c\) 的路径 \(p\), 它的边都没有标注与 \(i\) 相同的等价类的索引, 即 \(j\ne i, k\ne i\). 对于这条路径 \(p\), 可以得到 \[ Cond_i(p) = i\ne j\land j\ne k \] 然后将第9行中的 \(t\) 更新为 \[ t:= (i=i\land i\ne j\land i=k)\Longrightarrow b[i]=c[i]. \] 现在 上面的 \(t\) 被添加到上面的公式 2.1 中了. \(t\) 左边显然成立, 由此我们推出一个与 \(b[i]\ne c[i]\) 矛盾的条件. 因此, 我们证明了最初例子的不可满足性.

应当注意, 当没有这样一种链接的时候, 上述算法返回的约束为 \(\rm TRUE\). 在这种情况下, 数组理论 \(\hat{Th}\) 是可满足的. 否则, \(t\) 就是一个封锁子句(blocking clause), 也就是说, \(t\) 的命题骨架与 \(\hat{Th}\) 的是不一致的. 这样就保证了 \(DPLL(T )\) 程序的命题部分的进展.

3. 扩展规则的延迟实例化

前面所示算法生成的约束足以蕴涵各个数组元素之间所需的等价性. 为了获得可扩展数组理论的完整判定程序, 我们需要添加蕴涵整个数组之间相等的约束. 除了执行前一小节的算法, 还应执行下述算法, 它产生进一步的约束, 蕴涵数组项的相等性.

\[ \begin{aligned} &\mathbf{Algorithm\ 2:}\ \text{EXTENSIONAL-ARRAY-ENCODING}\\ &\mathbf{Input:}\quad\quad \text{A conjunction of array literals } \hat{Th}\\ &\mathbf{Output:}\quad\; \text{TRUE, or a valid array formula } t\ \text{that blocks } \hat{Th}\\ \\ &1.\; t:=\text{TRUE};\\ &2.\; \text{Compute equivalence classes of terms in } \hat{Th};\\ &3.\; \text{Construct the weak equivalence graph } G\ \text{from } \hat{Th};\\ &4.\; \mathbf{for}\; a,b\; \text{such that } a\;\text{and}\; b\ \text{are terms in } \hat{Th}\; \mathbf{do}\\ &5.\;\quad \mathbf{if}\; a\not\approx b\; \mathbf{then}\\ &6.\;\quad\quad\; \mathbf{for}\;\text{each simple path } p\in G\ \text{from } a\;\text{to } b\; \mathbf{do}\\ &7.\;\quad\quad\quad\quad \text{Let } S\; \text{be the set of edge labels of }p;\\ &8.\;\quad\quad\quad\quad t:=t\wedge (\bigwedge_{i\in S}Cond_i^u(p)\Longrightarrow a=b);\\ &9.\; \mathbf{return}\;t; \end{aligned} \]

推导两个数组项之间的相等性如下: 考虑 \(\hat{Th}\) 中所用不相等的数组项 \(a,b\), 以及 \(a\) 和 \(b\) 之间的任何相等链. 选择一个这样的链, 我们将其称为 \(p\), 并令 \(S\) 为该链中数组更新中使用的所有不同索引的集合. 对于所有索引 \(i\in S\), 执行以下操作:

1. 在 \(p\) 的第一个边上找到以 \(i\) 或索引 \(j\) 使得 \(j\approx i\) 的数组项. 用 \(first\) 表示该数组项, .并用 \(p'\) 表示该边之前的路径 \(p\) 的前缀.
2. 找到在最近一次更新后的数组项, 该数组标有 \(i\) 或索引 \(k\), 使得 \(k\approx i\). 用 \(last\) 表示该数组项, 并用 \(p''\) 表示该边之后的路径 \(p\) 的后缀.
3. 检查 \(fist[i]\) 与 \(last[i]\) 是否相等.

如果这适用于所有索引, 则 \(a\) 必等于 \(b\). \(G\) 中的这种链具有以下形式:

算法2 使用图 \(G\) 来检查是否存在这样的链, 如下所述: 它考虑了从 \(a\) 到 \(b\) 的所有路径 \(p\). 对于每个路径 \(p\), 它计算集合 \(S\). 然后将 \[ \bigwedge_{i\in S}Cond_i^u(p)\Longrightarrow a=b \]

作为约束添加到 \(t\) 中, 其中 \(Cond_i^u(p)\) 的定义如下: 如果在 \(p\) 中没有边的索引标签等于 \(i\), 则为 \[ Cond_i^u(p):=Cond_i(p). \] 否则, 这是索引 \(i\) 在 \(p\) 上的更新满足上述约束的条件, 其形式如下: \[ Cond_i^u(p):=Cond_i(p')\land first[i]=last[i]\land Cond_i(p''). \] 考虑输入到算法2 的公式: \[ \hat{Th}:=v=w \land b=a\{i\leftarrow v\}\land b\ne a\{i\leftarrow w\}. \] 上式具有不一致性. 预处理步骤是添加读写公理的第一部分的实例. 对于 \(\hat{Th}\) 中的理论文字, 我们可得 \[ a\{i\leftarrow v\}[i]=v\ {\rm and}\ a\{i\leftarrow w\}[i]=w. \] 接下来, 构造如下的弱等价图:

除其他外, 算法2 将 \(b\) 和 \(a\{i\leftarrow w\}\) 标识为数组项. 它们之间只有一条路径, 并且该路径的集合 \(S\) 是关于 \(\{i\}\) 的单例图. 数组项的 \(first\) 是 \(a\{i\leftarrow v\}\), 数组项的 \(last\) 是 \(a\{i\leftarrow w\}\). 请注意, \(p'\) 是从 \(b\) 到 \(a\{i\leftarrow v\}\) 的路径, 而 \(p''\) 为空. 我们可得 \[ Cond_i^u(p)=(a\{i\leftarrow v\}[i]=a\{i\leftarrow w\}[i]) \] 然后添加约束 \[ a\{i\leftarrow v\}[i]=a\{i\leftarrow w\}[i]\Longrightarrow b=a\{i\leftarrow w\} \] 到公式中去. 回想一下, 我们已经添加了约束 \(a\{i\leftarrow v\}[i]=v\) 和 \(a\{i\leftarrow w\}[i]=w\) 并假定在公式的所有模型中 \(v = w\). 等式逻辑的判定程序将确定 \(a\{i\leftarrow v\}[i]=a\{i\leftarrow w\}[i]\) 成立, 因此 \(DPLL(T)\) 将推断出 \(b=a\{i\leftarrow w\}\) 在该公式的任何模型中都必须为真, 这与原公式 \(\hat{Th}\) 的第三个文字矛盾. Qed