SMT求解器中的数据类型，同时支持正常加法、异或、或和运算

Question

我正在尝试解决一些关于布尔变量的非线性方程，同时我想计算hamming权重(即涉及布尔变量的正常相加)。

我正在使用Z3 Smt Sovler & Bitvec来做到这一点，但它似乎对可以传递到等式中的单项式的数量有一些限制。

因此，我正在寻找一些替代解决方案；

问题：

x1,x2,......, x100 = boolean variables

我要解决的是：

x1 + x2 + .... + x100 = 58

和一些非线性方程。我已经附加了一个示例代码来显示错误。

我请求您帮助我，因为我是新的Z3表面贴片求解器。

代码：

from z3 import *

N = [BitVec('n%d'%i,7) for i in range(40)]

EQ = [N[0] ^ N[13] ^ N[19] ^ N[35] ^ N[39] ^ N[2]&N[25] ^ N[3]&N[5] ^ N[7]&N[8] ^ N[14]&N[21] ^ N[16]&N[18] ^ N[22]&N[24] ^ N[26]&N[32] ^ N[33]&N[36]&N[37]&N[38] ^ N[10]&N[11]&N[12] ^ N[27]&N[30]&N[31] ==1 ]

print(EQ[0])

Output:
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ==
...

同时，如果我减少单项式的数量，那么它会给出正确的表达式。

Answer 1

这是由于漂亮的打印机限制了它的打印量(以减少大量输出)，而不是z3的内部限制。

您可以通过在from z3 import *后面添加以下行来提高限制

set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000)

您可以调整这些数字以满足您的需要，但对于所有感兴趣的实际问题，上述内容应该足够了。如果我将这一行添加到您的程序中，我会看到如下输出：

n0 ^
n13 ^
n19 ^
n35 ^
n39 ^
n2 & n25 ^
n3 & n5 ^
n7 & n8 ^
n14 & n21 ^
n16 & n18 ^
n22 & n24 ^
n26 & n32 ^
n33 & n36 & n37 & n38 ^
n10 & n11 & n12 ^
n27 & n30 & n31 ==
1

我猜这就是你所期待的。

如果您想在一行中查看所有内容，请使用以下设置：

set_option(max_args=10000000, max_width=1000000, max_lines=1, max_depth=10000000, max_visited=1000000)