近似位依赖分析：识别不可行的程序合成问题

# 近似位依赖分析：识别不可行的程序合成问题 ## 1. 引言 程序合成旨在构建满足声明性规范的程序。在计算机编程领域，基于位向量的程序合成是一项关键技术。然而，在合成过程中，常常会遇到一些问题，即整个搜索空间中可能不存在满足规范的程序，这类问题被称为不可行问题。不可行问题的处理通常比可行问题更具挑战性，因为合成器需要证明在整个解空间中都不存在符合要求的程序。 为了快速识别这些不可行问题，我们提出了一种基于位依赖分析的方法。以计算两个整数 \(x\) 和 \(y\) 的平均值并向上取整为例，人类程序员凭直觉知道需要进行除以 2 或右移 1 位的操作，但程序合成器缺乏这种直觉。我们可以通过检查规范的输入和输出位之间的依赖关系，来确定合成程序所需的操作。 ## 2. 基础知识 ### 2.1 位向量和位向量函数 固定宽度的位向量是由布尔变量组成的向量，其长度固定。位向量函数是将多个位向量作为输入，输出一个位向量的函数。常见的位向量函数包括位运算（如与、或、异或）、算术运算（如加、减、乘、除）和位移运算（如左移、右移）。 ### 2.2 基本位和布尔函数 输入变量 \(x_i\) 在函数 \(f\) 中是基本的，如果存在常数 \(c_1, ..., c_n\) 使得 \(f|_{x_i = 0}(c_1, ..., c_n) \neq f|_{x_i = 1}(c_1, ..., c_n)\)。布尔函数 \(f\) 可以用 Zhegalkin 多项式唯一表示： \[f(x_1, ..., x_n) = \sum_{K \subseteq \{1, ..., n\}} a_K \land \prod_{i \in K} x_i\] 其中 \(a_K \in \{0, 1\}\)。例如，\(\neg(x_1 \land x_2) = 1 \oplus (x_1 \land x_2)\)，其中 \(a_{\{1\}} = a_{\{2\}} = 0\)，\(a_{\varnothing} = a_{\{1, 2\}} = 1\)。 ### 2.3 图论基础 在本文中，无向图不允许有平行边，而有向图允许。对于图 \(G\)，\(N(X)\) 表示集合 \(X\) 中所有顶点的邻居集合。二分图 \(G\)（分区为 \(\{A, B\}\)）包含 \(A\) 中所有顶点的匹配，当且仅当对于所有 \(X \subseteq A\)，有 \(|N(X)| \geq |X|\)（Hall 婚姻定理）。 ## 3. 基本位的近似计算 由于计算任意函数的所有基本位是 NP 完全问题，我们提出了两种下近似和一种上近似方法。 ### 3.1 下近似 UA1 下近似 \(UA1\) 只考虑 \(|K| \leq 1\) 的系数 \(a_K\)。对于常数 1 和位 \(x_i\)，计算 \(UA1\) 的规则如下： - \(UA1(1) = \{1\}\) - \(UA1(x_i) = \{x_i\}\) 对于 \(f = g \oplus h\)，\(UA1(g \oplus h) = UA1(g) \triangle UA1(h)\)，其中 \(\triangle\) 是对称集合差。对于 \(f = g \land h\)，\(UA1(g \land h) = (UA1(g) \cap UA1(h)) \triangle NT(g, h) \triangle NT(h, g)\)，其中： \[NT(k_1, k_2) = \begin{cases} UA1(k_1) \setminus \{1\} & \text{if } 1 \in UA1(k_2) \\ \varnothing & \text{otherwise} \end{cases}\] ### 3.2 下近似 UA2 我们可以使用 \(UA1\) 来计算 \(|K| \leq 2\) 的系数 \(a_K\) 的集合 \(UA2\)。对于函数 \(f\) 的每个位 \(x_i\)，通过 Reed - Muller 分解，\(UA1(f|_{x_i = 0} \oplus f|_{x_i = 1})\) 包含所有使得 \(a_{\{i, j\}} = 1\) 的 \(x_j\)。通过取所有位 \(x_i\) 的这些基本位的并集（再加上 \(UA1(f)\)），我们得到 \(UA2(f)\)。 ### 3.3 上近似 OA 上近似 \(OA\) 包含可能出现在某些集合 \(K\) 中且 \(a_K = 1\) 的 \(x_i\)，以及如果 \(a_{\varnothing} = 1\) 则包含 1。对于常数 1 和位 \(x_i\)，计算 \(OA\) 的规则如下： - \(OA(1) = \{1\}\) - \(OA(x_i) = \{x_i\}\) 对于 \(f = g \oplus h\)，\(OA(g \oplus h) = OA(g) \cup OA(h)\)。对于 \(f = g \land h\)， \[OA(g \land h) = \begin{cases} \varnothing & \text{if } OA(g) = \varnothing \text{ or } OA(h) = \varnothing \\ OA(g) \cup OA(h) & \text{otherwise} \end{cases}\] ## 4. 标记不可行的程序合成问题 ### 4.1 位依赖形状 我们发现输入变量的基本位通常遵循四种规则模式，我们称之为位形状： - **简单形状（\(\bullet\)）**：第 \(i\) 个输出位仅基于第 \(i\) 个输入位，例如与运算。 - **上升形状（\(\uparrow\)）**：输入位 \(j \leq i\) 影响第 \(i\) 个输出位，例如加法运算。 - **下降形状（\(\downarrow\)）**：第 \(i\) 个输出位依赖于输入位 \(j \geq i\)，例如右移运算。 - **块形状（\(\blacksquare\)）**：任意输入位影响输出位，例如下除法运算。 这些形状形成一个格，较大的形状包含较小形状的所有输入 - 输出依赖关系。规范函数的输入变量形状或操作数的形状是最适合其近似基本位的最小形状。 ### 4.2 树状上界 如果存在一个满足规范函数 \(f\) 的上界程序，那么也存在一个其基础无向图是树的上界程序。因此，我们可以只在树状程序的搜索空间中进行搜索，以减少搜索的复杂度。 ### 4.3 变量到使用位置的二分匹配 为了避免在树状程序的搜索中进行冗余的配置检查，我们将变量替换为占位符节点，将问题转化为二分匹配问题。通过计算最大匹配的大小 \(\nu\)，我们可以有效地判断是否存在上界。 \[ \nu(P) = |L(P)| - \max_X(|L(P, \downarrow X)| - |V(\downarrow