在z3中高效查找BitVec权重（即访问位向量的位）

Question

我现在正在使用Python的z3库来计算比特向量的权重。

在寻找更简单的方法时，我决定自己实现一个计算比特向量st1权重的函数，具体做法如下：

Sum([( (st1 & (2**(i)))/(2**(i)) ) for i in range(bits)])

我想问的是，有没有更简单或更高效的方法呢？

我的问题是，我有一些包含1500多个这种权重约束的情况，我希望确保我的做法尽可能高效。

补充说明：我想计算的东西有个专门的名字（叫做汉明重量），我知道在一些命令式语言中有非常高效的实现方法，但我最终想知道的是，是否有任何底层的方法可以访问z3比特向量的单个比特。

Answer 1

你可以试试用递归的方法，也许你可以看看这个动态规划的内容。

Answer 2

我稍微玩了一下你在问题中提到的例子：

• z3 在解析 SAT 模型时偶尔会卡住

我觉得那些无法解决的情况很难处理，因为问题似乎有很多对称性。如果真是这样，我们可以通过加入“打破对称性的约束”来提高性能。Z3 对于这种问题无法自动打破对称性。

这里有一个小的编码改进。表达式 ((st1 & (2**(i)))/(2**(i)) 实际上是在提取第 i 位。我们可以用 Extract(i, i, st1) 来提取第 i 位。结果是一个大小为 1 的位向量。然后，我们需要“扩展”它，以避免溢出。你问题中的位向量最多有 28 位。所以，5 位就足够避免溢出。因此，我们可以用 ZeroExt(4, Extract(i, i, st1))。也就是说，我们把

Sum([( (st1 & (2**(i)))/(2**(i)) ) for i in range(bits)])

替换为

Sum([ ZeroExt(4, Extract(i,i,st1)) for i in range(bits) ])

我得到了大约 2 倍的速度提升。不过，Z3 还是无法解决 6 位的无法满足实例 :(