Bit Vectors (2)
位向量演算
算术运算符
算术运算符的约束通常依照那些作为电路的运算符的实现. 实验说明了很多候选的电路设计往往是最简单的那种在验证的时候, SAT 求解器的负担最小. 先定义一位加法器, 也就是全加器(full adder).
全加器. 一个全加器使用两个函数来进行逻辑定义的, 进位(carry)和求和(sum). 这两个函数都接收三个输入\(a,b,cin\). 函数carry计算加法器结果的进位, 函数sum计算和: \[ \begin{aligned} sum(a,b,cin)&\doteq (a\oplus b)\oplus cin,\\ carry(a,b,cin)&\doteq (a\land b)\lor ((a\oplus b)\land cin). \end{aligned} \] 我们可以将该定义扩展到任意长度的位向量的加法器.
进位定义. 令 \(x\) 和 \(y\) 表示两个 \(l\) 个比特长度的位向量, \(cin\) 表示一个单比特位. 进位 \(c_0\) 和 \(c_l\) 递归地定义如下: \[ c_i \doteq \begin{equation} \left\{ \begin{array}{lr} cin:i=0\\ carry(x_{i-1},y_{i-1},c_{i-1}):otherwise. \end{array} \right. \end{equation} \] 加法器. 一个 \(l\) 比特的加法器, 将两个 \(l\) 比特的位向量 \(x,y\) 和一个进位 \(cin\) 映射为 对应的 和(sum) 与一个输出进位. 令 \(c_i\) 表示第 \(i\) 个进位. 函数add用进位 \(c_i\) 来定义: \[ \begin{aligned} add(x,y,cin)&\doteq \langle result, cout\rangle,\\ result_i &\doteq sum(x_i,y_i,c_i)\ for\ i\in \{0,...,l-1\},\\ cout &\doteq c_n. \end{aligned} \] 该结构的等效电路称作行波进位加法器(ripple carry adder). 该加法器可以很容易地用一个带有进位 \(cin=0\) 的加法器实现针对 \(t=a+b\) 的约束: \[ \bigwedge_{i=0}^{l-1}(add(a,b,0).result_i\Longleftrightarrow e(t)_i). \] 同时加法器可以通过归纳地证明上面的约束成立, 当且仅当 \(\langle a\rangle_U + \langle b\rangle_U = \langle e(t)\rangle_U\ \rm mod\ 2^l\), 同时说明了约束与之前说明的语义相符.
通过使用以下约束, 在同一电路中实现减法 \(t=a-b\): \[ \bigwedge_{i=0}^{l-1}(add(a,\thicksim b,1).result_i \Longleftrightarrow e(t)_i). \] 同样的, 该实现利用了事实: \(\langle (\thicksim b) + 1\rangle_S = -\langle b\rangle_S \rm\ mod\ 2^l\).
关系运算符
等式 \(a=_{l}b\) 用简单的合取式实现: \[ \bigwedge_{i=1}^{l-1} a_i = b_i \Longleftrightarrow e(t). \] 如上所述, 将 \(a\lt b\) 的大小关系转换为 \(a-b\lt 0\). 并为减法建立加法器. 因此, \(b\) 取反, 加法器的进位设置为true. \(a\lt b\) 的结果取决于编码. 对于无符号操作数, 如果加法器的进位 \(cout\) 为FALSE, 则 \(a\lt b\) 成立: \[ \langle a\rangle_U \lt \langle b\rangle_U \Longleftrightarrow \neg add(a,\thicksim b,1).cout. \] 如果是带符号的操作数, 当且仅当 \((a_{l-1}=b_{l-1})\ne cout\) 时, \(a\lt b\) 成立: \[ \langle a\rangle_S \lt \langle b\rangle_S \Longleftrightarrow (a_{l-1}\Longleftrightarrow b_{l-1})\oplus add(a,b,1).cout. \] 涉及混合编码的比较是通过将两个操作数都扩展一位, 然后进行带符号的比较来实现的.
移位
我们称移位运算符的左侧操作数(要移位的向量)的宽度为移位的宽度(width of the shift), 而右侧操作数的宽度为移位距离的宽度(width of the shift distance). 我们按照以下方式限制左右移位: 移位的宽度 \(l\) 必须为2的幂次, 并且移位距离 \(n\) 的宽度必须为 \(\log_2l\). 在这种限制下, 可以通过使用以下称为桶形移位器(barrel shifter)的构造来实现左右移位. 该移位操作分为 \(n\) 个阶段. 阶段 \(s\) 可以将操作数移动 \(2^s\) 个比特或者保持不动. 函数 \(ls\) 针对阶段 \(s \in \{-1,...,n-1\}\) 递归地定义如下: \[ ls(a_{[l]}, b_{[n]U},-1)\doteq a, ls(a_{[l]}, b_{[n]U}, s)\doteq \\ \lambda i\in\{0,...,l-1\}. \begin{equation} \left \{\begin{array}{lr} (ls(a,b,s-1))_{i-2^s}&:&i\ge 2^s\land b_s\\ (ls(a,b,s-1))_i&:&\neg b_s\\ 0&:&otherwise. \end{array} \right. \end{equation} \] 桶形移位器地构造仅需要时间复杂度为 \(O(n\log n)\) 的逻辑操作, 而原始的实现方式要 \(O(n^2)\) 时间复杂度.
乘法和除法
乘法器可以按照最简单的电路设计来实现, 它采用移位加法的思想(shift-and-add idea). 为阶段 \(s\in \{-1,...,n-1\}\) 递归地定义函数 mul, 其中 \(n\) 表示第二个操作数的宽度: \[ mul(a,b,-1)\doteq 0,\\ mul(a,b,s)\doteq mul(a,b,s-1)+(b_s ? (a<<s):0). \] 除法 \(a/_Ub\) 通过额外添加两个约束来实现: \[ \begin{aligned} &b\ne 0\Longleftrightarrow e(t).b+r=a,\\ &b\ne 0\Longleftrightarrow r\lt b. \end{aligned} \] 变量 \(r\) 是一个新的位向量, 其宽度与 \(b\) 相同, 并包含余数. 有符号除法和模运算以类似的方式实现.
增量 Bit Flattening 算法
对于某些运算来说, BV-Constraint 生成的公式可能很大. 除了这些公式的绝对大小之外, 它们的对称性和连通性也是最新的命题 SAT 求解器的决策启发式方法的负担. 随之而来的后果就是, 带乘法运算的公式通常很难求解. 其他算术运算符(例如除法和模)也会有类似的结果.
比如说, 考虑如下位向量公式: \[ a\cdot b=c \land b\cdot a\ne c \land x\lt y \land x\gt y. \] 当这个公式被编码成CNF时, 一个宽度为32位的 SAT 实例就会产生约11000个变量. 该公式显然是不可满足的. 有两个原因: 最开始的两个合取的式子矛盾, 同样地, 后两个合取的式子也是矛盾的. 大多数 SAT 求解器的决策启发式方法倾向于首先对经常使用的变量进行拆分, 因此倾向于对 \(a\), \(b\)和 \(c\) 进行判定. 因此, 求解器试图在包括两个乘法运算的困难部分上显示该公式的不满足性. 该公式仅包含两个关系运算符的"简单"部分被忽略了. 大多数命题 SAT 求解器都不能在合理的时间内解决该公式.
因此, 在许多情况下, 逐步建立扁平化的公式 \(\mathcal{B}\) 是有益处的. 算法1是根据如下想法的实现: 正如之前, 从公式 \(\varphi\) 的命题骨架开始. 然后, 我们为"廉价"的运算符添加约束, 并为"昂贵"的运算符省略约束. 按位运算符通常是廉价的, 而算术运算符很昂贵. 缺少约束的编码可以视为对公式 \(\varphi\) 的抽象. 那么, 当前扁平化的公式 \(\mathcal{B}\) 会被传给一个命题 SAT 求解器. 如果, \(\mathcal{B}\) 是不可满足的, 那么原公式 \(\varphi\) 也是不可满足的. 将公式后半部分的约束条件添加到 \(\mathcal{B}\) 中后, 编码后的公式就变得不可满足, 并且会得出结论, 在不考虑乘法运算的情况下原公式 \(\varphi\) 是不可满足的.
\[ \begin{aligned} &\mathbf{Algorithm\ 1:\ }{\rm INCREMENTAL\mbox{-}BV\mbox{-}FLATTENING}\\ &\mathbf{Input:}\ {\rm A\ formula}\ \varphi\ {\rm in\ bit\mbox{-}vector\ logic}\\ &\mathbf{Output:}\ {\rm ''Satisfiable''\ if\ the\ formula\ }\ {\rm is\ satisfiable,\ and\ ''Unsatisfiable''\ otherwise}\\ \\ &1.\hspace{2mm}\mathbf{function}\ {\rm INCREMENTAL\mbox{-}BV\mbox{-}FLATTENING}(\varphi)\\ &2.\hspace{10mm} \mathcal{B}:=e(\varphi);\hspace{55mm} \triangleright\ {\rm propositional\ skeleton\ of\ }\varphi\\ &3.\hspace{10mm}\mathbf{for\ }{\rm each\ } t_{[l]}\in T(\varphi)\ \mathbf{do} \\ &4.\hspace{18mm}\mathbf{for\ }{\rm each\ } i\in \{0,...,l-1\}\ \mathbf{do} \\ &5.\hspace{26mm}{\rm set}\ e(t)_i\ {\rm to\ a\ new\ Boolean\ variable}; \\ &6.\hspace{10mm}\mathbf{while\ } {\rm (TRUE)}\ \mathbf{do}\\ &7.\hspace{18mm}\alpha := {\rm SAT\mbox{-}SOLVER}(\mathcal{B}); \\ &8.\hspace{18mm}\mathbf{if\ }\alpha={\rm ''Unsatisfiable''}\ \mathbf{return} \\ &9.\hspace{26mm}\mathbf{return}\ {\rm ''Unsatisfiable''}; \\ &10.\hspace{16mm}\mathbf{else\ }\\ &11.\hspace{24mm}{\rm Let\ } I\subseteq T(\varphi)\ {\rm be\ the\ set\ of\ terms\ that\ are}\\ &\hspace{38mm}{\rm inconsistent\ with\ the\ satisfying\ assignment}; \\ &12.\hspace{24mm}\mathbf{if}\ I=\emptyset\ \mathbf{then} \\ &13.\hspace{30mm}\mathbf{return}\ {\rm ''Satisfiable''};\\ &14.\hspace{24mm}\mathbf{else} \\ &15.\hspace{30mm}{\rm Select\ ''easy''\ } F'\subseteq I; \\ &16.\hspace{30mm}\mathbf{for}\ {\rm each\ } t_{[l]}\in F'\ \mathbf{do}\\ &17.\hspace{38mm}\mathcal{B}:=\mathcal{B}\ \wedge\ {\rm BV\mbox{-}CONSTRAINT}(e,t);\\ \end{aligned} \]
如果公式 \(\mathcal{B}\) 是可满足的, 以下两种情况之一适用:
- 原公式 \(\varphi\) 是不可满足的, 但是需要一个或多个被省略的约束条件说明这一点.
- 原公式 \(\varphi\) 是可满足的.
为了区分这两种情况, 我们可以检查 SAT 求解器产生的可满足赋值是否满足省略的约束. 由于我们可能已经移除了一些变量, 所以可能要对可满足的赋值进行扩展, 将缺失的值设置为某个常数, 例如, 0. 如果此赋值满足所有约束, 则第二种情况适用, 并且算法终止.
如果不是这样, 那么被省略的一个或多个约束条件与 SAT 求解器提供的赋值不一致.我们用 \(I\) 来表示这些项的集合. 算法通过选择其中的一些项, 将其约束条件添加到公式 \(\mathcal{B}\) 中, 并重复进行. 算法终止, 因为我们每一次迭代都会严格地添加更多的约束条件. 在最坏的情况下, \(T(\varphi)\) 中的所有约束条件都被添加到编码中.
在许多情况下, 省略特定运算符的约束可能会导致扁平化的公式太弱, 从而被太多的虚假模型所满足. 另一方面, 全约束可能会给 SAT 求解器带来太多负担. 在全约束的最大强度和完全省略约束之间的折中办法, 是用未解释的函数替换位向量上的函数.当在检查两个模型的等价性时, 这种技术特别有效. 比如说, 令 \(a_1\ op\ b_1\) 和 \(a_2\ op\ b_2\) 为两项, 其中 \(op\) 是二元运算符. 用一个新的未解释的符号 \(G\) 来替换运算符 \(op\) 得到 \(G(a_1,b_1)\) 和 \(G(a_2,b_2)\). 得出的公式是抽象的, 并不包含对应于 \(op\) 的扁平化的约束条件.