1

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

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

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

我的问题相对简单，有没有更简单/更有效的方法？

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

编辑：我将添加以下说明，我试图计算的内容有一个名称（它是汉明权重），我知道有非常有效的方法可以在命令式语言中实现功能，但最终我正在寻找什么是否有任何底层方法可以访问 z3 位向量的各个位。

4

2 回答 2

1

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

我相信 unsat 实例很难解决，因为这个问题似乎有很多对称性。如果是这种情况，我们可以通过包含“对称破坏约束”来提高性能。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 位 unsat 实例 :(

于 2013-02-07T05:28:52.130 回答
-1

你应该尝试使用递归方法，也许你可以看看这个动态编程

于 2013-02-06T14:22:28.870 回答