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

编程问答 2022-05-28

问题描述

我正在尝试解决一些关于布尔变量的非线性方程，同时我想计算汉明权（即涉及布尔变量的正常加法）。

我正在使用 Z3 Smt Sovler & Bitvec 来这样做，但似乎对可以传递给方程的单项式数量有一些限制。

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

问题：

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

我必须解决：

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

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

我请求您帮助我，因为我是 Z3 smt 求解器的新手。

代码：

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:
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ==
...

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

解决方法

这是由于漂亮打印机限制了它的打印量（以减少大量输出），而不是 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_visited=1000000)
jupyter-notebookpythonsatsmtz3