形式化12：位向量

向量"/>

形式化12：位向量

位向量(bit vector)

位向量 b b b是长度为 l l l的 0 / 1 0/1 0/1序列:

其中 b l − 1 b_{l-1} bl−1​是最高有效位, b 0 b_0 b0​是最低有效位.而 l l l是一个预先定义的常量

前景

在JDK源码的二分查找中,有如下的语句:

int middle = (low+high)/2;

而由于计算机中的数据有确定的位宽,因此可能产生溢出,如下是解决方案

t0 = (x & y) + ((x ^ y) >> 1);
t  = t0 + (LShR(t0, 31) & (x ^ y))

语法

⊕ : : = + ∣ − ∣ ∗ ∣ / ∣ < < ∣ > > ∣ > > > ∣ & ∣ ∣ ∣ x o r E : : = x ∣ c ∣ E ⊕ E ∣ ∼ E R : : = E = E ∣ E ≤ E ∣ E < E P : : = R ∣ ¬ P ∣ P ∧ P \begin{align} \oplus::=&\ +\ |\ -\ |\ *\ |\ /\ |\ <<\ |\ >>\ |\ >>>\ |\ \&\ |\ |\ |\ xor \\ E::=&\ x\ |\ c\ |\ E\oplus E\ |\ \sim E \\ R::=&\ E=E\ |\ E\le E\ |\ E < E \\ P::=&\ R \\ |&\ \neg P \\ |&\ P\land P \end{align} ⊕::=E::=R::=P::=∣∣​ + ∣ − ∣ ∗ ∣ / ∣ << ∣ >> ∣ >>> ∣ & ∣ ∣ ∣ xor x ∣ c ∣ E⊕E ∣ ∼E E=E ∣ E≤E ∣ E<E R ¬P P∧P​​

例如:
x = = 1 ∧ y = = 3 ∧ x & y = 0 x==1 \land y==3 \land x\&y=0 x==1∧y==3∧x&y=0
是UNSAT的! 用z3描述就是:

x, y = BitVecs('x y', 32)  # 32位宽度
solve(x == 1, y == 3, x & y == 0)

位的解释

无符号数 : ⟨ b ⟩ u = ∑ i = 0 l − 1 b i × 2 i 有符号数 : ⟨ b ⟩ s = − b l − 1 × 2 l − 1 + ∑ i = 0 l − 2 b i × 2 i \begin{align} &无符号数: \langle b \rangle _u = \displaystyle\sum_{i=0}^{l-1} b_i \times 2^i \\ &有符号数: \langle b \rangle _s = -b_{l-1} \times 2^{l-1} + \displaystyle\sum_{i=0}^{l-2} b_i \times 2^i \end{align} ​无符号数:⟨b⟩u​=i=0∑l−1​bi​×2i有符号数:⟨b⟩s​=−bl−1​×2l−1+i=0∑l−2​bi​×2i​​

需要注意的是:位向量是有位数限制的,例如以下e求解:

x, y = BitVecs('x y', 8)
solve(x + y == 1024)
# z3 output
[x = 0, y = 0]

之所以结果为x=0,y=0是因为1024=0b100 0000 0000,而x,y宽度仅为8,因此求解器将x+y=1024转化为了x+y=1024%8 => x+y=0,即:

a + u b = c ≜ ⟨ a ⟩ u + ⟨ b ⟩ u = ⟨ c ⟩ u m o d 2 l a − u b = c ≜ ⟨ a ⟩ u − ⟨ b ⟩ u = ⟨ c ⟩ u m o d 2 l a + s b = c ≜ ⟨ a ⟩ s + ⟨ b ⟩ s = ⟨ c ⟩ s m o d 2 l a − s b = c ≜ ⟨ a ⟩ s − ⟨ b ⟩ s = ⟨ c ⟩ s m o d 2 l − a = b ≜ − ⟨ a ⟩ s = ⟨ b ⟩ s m o d 2 l a × u b = c ≜ ⟨ a ⟩ u × ⟨ b ⟩ u = ⟨ c ⟩ u m o d 2 l a ÷ u b = c ≜ ⟨ a ⟩ u ÷ ⟨ b ⟩ u = ⟨ c ⟩ u m o d 2 l a × s b = c ≜ ⟨ a ⟩ s × ⟨ b ⟩ s = ⟨ c ⟩ s m o d 2 l a ÷ s b = c ≜ ⟨ a ⟩ s ÷ ⟨ b ⟩ s = ⟨ c ⟩ s m o d 2 l \begin{align} &a+_ub=c\quad &\triangleq \quad &\langle a \rangle _u + \langle b \rangle _u = \langle c \rangle _u\ mod\ 2^l& \\ &a-_ub=c\quad &\triangleq \quad &\langle a \rangle _u - \langle b \rangle _u = \langle c \rangle _u\ mod\ 2^l& \\ &a+_sb=c\quad &\triangleq \quad &\langle a \rangle _s + \langle b \rangle _s = \langle c \rangle _s\ mod\ 2^l& \\ &a-_sb=c\quad &\triangleq \quad &\langle a \rangle _s - \langle b \rangle _s = \langle c \rangle _s\ mod\ 2^l& \\ &-a=b\quad &\triangleq \quad&-\langle a \rangle _s = \langle b \rangle _s \ mod\ 2^l& \\ &a\times_ub=c\quad &\triangleq \quad &\langle a \rangle _u \times \langle b \rangle _u = \langle c \rangle _u\ mod\ 2^l& \\ &a\div_ub=c\quad &\triangleq \quad &\langle a \rangle _u \div \langle b \rangle _u = \langle c \rangle _u\ mod\ 2^l& \\ &a\times_sb=c\quad &\triangleq \quad &\langle a \rangle _s \times \langle b \rangle _s = \langle c \rangle _s\ mod\ 2^l& \\ &a\div_sb=c\quad &\triangleq \quad &\langle a \rangle _s \div \langle b \rangle _s = \langle c \rangle _s\ mod\ 2^l& \\ \end{align} ​a+u​b=ca−u​b=ca+s​b=ca−s​b=c−a=ba×u​b=ca÷u​b=ca×s​b=ca÷s​b=c​≜≜≜≜≜≜≜≜≜​⟨a⟩u​+⟨b⟩u​=⟨c⟩u​ mod 2l⟨a⟩u​−⟨b⟩u​=⟨c⟩u​ mod 2l⟨a⟩s​+⟨b⟩s​=⟨c⟩s​ mod 2l⟨a⟩s​−⟨b⟩s​=⟨c⟩s​ mod 2l−⟨a⟩s​=⟨b⟩s​ mod 2l⟨a⟩u​×⟨b⟩u​=⟨c⟩u​ mod 2l⟨a⟩u​÷⟨b⟩u​=⟨c⟩u​ mod 2l⟨a⟩s​×⟨b⟩s​=⟨c⟩s​ mod 2l⟨a⟩s​÷⟨b⟩s​=⟨c⟩s​ mod 2l​​​

求解位向量的SMT问题:比特爆炸算法(Bit-Blasting)

• a , b , c a,b,c a,b,c都是l位宽的比特向量,如何求解a=1 /\ b=2 /\ a&b=1是否可满足?

1. 建立抽象语法树,将所有变量/常量的位展开,例如x=b0,...,bn,图中矩形和椭圆分别圈住了相同的变量,相同的变量展开也是相同的
   
2. 以后序遍历的方式建立约束,并将约束添加到一个约束集合中
3. 将所有的约束丢给求解器进行求解,决策过程如下
   

• 伪代码描述

C = {}  // 约束集合
bitBlast(P){ // 将命题转化为原子布尔值blastProp(P);// 生成约束genConsProp(P);
}blastProp(P){ if P is (e1 = e2) {  // 相等关系// 对于原子命题，遍历表达式blastExp(e1); blastExp(e2); } else if P is (P1 /\ P2) { // 合取关系// 递归blastProp(P1); blastProp(P2);}
}blastExp(e){ if e is x:  // 变量return (b0, b1, …, bn); // 返回布尔变量集合if e is c:  // 常量return (b0, b1, …, bn); if e is e1+e2: // 相加(b0, …, bn) = blastExp(e1); (c0, …, cn) = blastExp(e2); return (d0, …, dn); // d由b和c计算得来,需要考虑进位等情况// other cases are similar
}genConsProp(P){ if P is (e1=e2): genConsExp(e1); genConsExp(e2); C ∪= {x0=y0, …, xn=yn};  // 求并集else if P is (P1 ∧ P2): genConsProp(P1); genConsProp(P2);
}genConsProp(e) {switch(e){ case (x&y): C ∪= {z0=x0 ∧ y0, z1=x1 ∧ y1, …, zn=xn ∧ yn} break;case (x|y): C ∪= {z0=x0 ∨ y0, z1=x1 ∨ y1, …, zn=xn ∨ zn} break;case (~x): C ∪= {z0=~x0, z1=~x1, …, zn=~xn}; break;case (x+y): c0=F ∧ r0=xor(x0,y0,c0) ∧ c1=(x0 ∧ y0)\/(xor(x0,y0) ∧ c0)r1=xor(x1,y1,c1) ∧ c2=(x1 ∧ y1)\/(xor(x1,y1) ∧ c1) ......break;// 转换为加法case (x-y): genConsProp(x+(-y));                break;case (x*y): genConsProp(y+...+y);               break;// 除数!=0  商*除数+余数=被除数  余数<被除数case (x/y): genConsProp(y!=0 ∧ d*y+r=x ∧ r<y);  break;}
}

其中需要特别注意的是加法，它的展开就会很复杂:

• 算法的改进
  从上面的描述中可以看出,即使是很简单的运算也会产生大量的约束,而对于加减乘除则更为复杂,为了减少计算量,可以采用一种启发式的策略优化这种算法,例如对于命题a*b=c /\ b*a!=c /\ y=x&z /\ y!=x&z我们可以:

1. 先计算简单的部分y=x&z /\ y!=x&z,如果SAT,那么执行第2步,如果UNSAT,直接返回UNSAT
2. 将上一步中SAT的模型代入a*b=c /\ b*a!=c中,如果SAT,返回此模型,否则执行第3步
3. 添加约束b*a!=c仅需求解
4. …

也就是说从简单到难一点点计算,如果得到结果,那么就不必继续

应用

验证费马大定理: 在 n ≥ 3 n \ge 3 n≥3的情况下,等式 a n + b n = c n a^n+b^n=c^n an+bn=cn无解

# 此程序验证n=3的情况
solver = Solver()
a, b, c = BitVecs('a b c', 64)  # 三个宽为64位的比特向量
cons = []
cons.append(a & 0xffffff0000 == 0)  # 限制数据范围为16位
cons.append(b & 0xffffff0000 == 0)  # 这样a*b*c最大就是48位
cons.append(c & 0xffffff0000 == 0)  # 不会到达64位产生溢出
cons.append(a != 0)
cons.append(b != 0)
cons.append(c != 0)
cons.append(a * a * a + b * b * b == c * c * c)
solver.add(cons)

当然上面的算术只验证了一定范围内的数据,z3显然是不可能验证无限域的