在 z3 中有效地查找 BitVec 权重(也就是访问位向量的位) [英] Finding BitVec weight efficently (aka access to bits of a bitvector) in z3

问题描述

我目前正在使用 z3 的 python api 计算位向量的权重.

I'm currently computing the weight of bitvectors using the python api for z3.

在通过 python API 搜索更直接的方法后，我正在以下列方式实现位向量 st1 的权重函数:

After searching through the python API for more straight forward method, I'm implementing the weight function for a bitvector st1 in the following manner:

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

我的问题比较简单，有没有更简单/更有效的方法?

My question is relatively straight-forward, is there an easier/more efficient way?

我遇到了包含 1500 多个此类重量限制的问题，并希望确保我尽可能高效地做事.

I have problems which contain 1500+ of these weight constraints and would like to make sure I'm doing things as efficiently as possible.

我将添加以下说明，我试图计算的有一个名称(它是汉明权重)，我知道在命令式语言中有超高效的实现功能的方法，但是 最终我要寻找的是是否有任何底层方法可以访问 z3 位向量的各个位.

推荐答案

我对您在问题中发布的示例进行了一些操作:

I played a little bit with the example you posted in the question:

• z3 伪随机挂起SAT模型

我相信 unsat 实例很难解决，因为这个问题似乎有很多对称性.如果是这种情况，我们可以通过包含对称破坏约束"来提高性能.对于此类问题，Z3 无法自动破坏对称性.

I believe the unsat instances are hard to solve because the problem seems to have many symmetries. If that is the case, we can improve the performance by including "symmetry breaking constraints". Z3 can't break the symmetries automatically for this kind of problem.

这是一个小的编码改进.表达式 ((st1 & (2**(i)))/(2**(i)) 本质上是提取第 i 位.我们可以使用 Extract(i, i, st1) 提取第 i 个位.结果是大小为 1 的位向量.然后，我们必须扩展"它以避免溢出.您问题中的位向量位于最多28位.所以，5位就足以避免溢出.因此，我们可以使用ZeroExt(4, Extract(i, i, st1)).也就是说，我们替换

Here is a minor encoding improvement. The expression ((st1 & (2**(i)))/(2**(i)) is essentially extracting the i-th bit. We can use Extract(i, i, st1) to extract the i-th bit. The result is a Bit-vector of size 1. Then, we have to "expand" it to avoid overflows. The bit-vectors in your problem have at most 28 bits. So, 5 bits is enough to avoid overflows. Therefore, we can use ZeroExt(4, Extract(i, i, st1)). That is, we replace

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 位 unsat 实例:(

I get a modest 2x speedup. So, Z3 still cannot solve the 6 bits unsat instance :(

这篇关于在 z3 中有效地查找 BitVec 权重(也就是访问位向量的位)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！