布尔组合的体积计算：算法、应用与实验

### 布尔组合的体积计算：算法、应用与实验 #### 1. 体积计算的优化思路 在计算布尔组合公式的体积时，我们发现理论不一致的赋值（无论是否在命题上满足公式）并不影响总体积。基于此观察和相关命题，我们可以减少对体积计算过程的调用次数。具体做法是，借助 SMT 求解器列出所有可行赋值，然后进行可能的组合形成束（bunches），必要时纳入一些理论不一致的赋值。不过，SMT 求解器不会明确提供理论不一致的赋值，因此需要额外调用理论求解器。 #### 2. 具体算法 我们的方法是在 SMT(LAC) 求解器的决策过程中实现体积计算。当 SMT 求解器找到一个可行赋值时，会尝试找到一个更小的赋值，这个赋值仍在命题上满足公式，即最小立方体（minimum cube）。 ##### 2.1 最小立方体的定义 假设 $\alpha$ 是公式 $\varphi$ 的一个可行赋值，若赋值 $\alpha_{mc}$ 满足以下两个条件，则称其为 $\alpha$ 的最小立方体： 1. $\alpha_{mc} \subseteq \alpha$ 且 $\alpha_{mc} \vDash PS\varphi$。 2. $\forall\alpha'(\alpha' \vDash PS\varphi \to \alpha' \not\subset \alpha_{mc})$。 对于可行赋值 $\alpha$ 及其最小立方体 $\alpha_{mc}$，由相关命题可知，$volume(\alpha_{mc})$ 包含 $volume(\alpha)$ 以及可能的其他可行赋值的体积。因此，计算 $volume(\alpha_{mc})$ 比计算 $volume(\alpha)$ 更有价值。 ##### 2.2 寻找最小立方体的方法 目前我们使用一种简单的方法来寻找最小立方体，即依次检查 $\alpha$ 中每个文字的冗余性。如果移除某个文字 $l_i$ 后，$\alpha$ 仍能使 $PS\varphi$ 为真，则立即从 $\alpha$ 中删除 $l_i$，并对修改后的 $\alpha$ 检查下一个文字。可以证明，最终结果是原始赋值的最小立方体。 ##### 2.3 体积计算算法 以下是具体的体积计算算法： ```python Boolean Formula PS = PSφ; volume = 0; while TRUE do if BCP() == CONFLICT then backtrack - level = AnalyzeConflict(); if backtrack - level < 0 then return volume; end if backtrack to backtrack - level; else α = current assignment; if α |= PS then if Th(α) is inconsistent then backtrack to the latest decision variable; else for all literal li ∈ α do if li is a decision variable or its negation then α′ = α - {li}; if α′ |= PS then α = α′; end if end if end for volume += VOLcompute(α); Add ¬α to PS; end if else choose a Boolean variable and extend the current assignment; end if end if end while ``` #### 3. 算法的正确性证明 - **命题 2**：给定可行赋值 $\alpha$ 和其中的文字 $l_i$，如果 $l_i$ 不是决策变量或其否定，则它必须出现在 $\alpha$ 的任何最小立方体中。 - **定理 1**：上述算法能计算出公式 $\varphi$ 的体积。证明过程主要从两个方面进行：一是任