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

Question

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

我正在使用 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:
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ==
...

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

Answer 1

这是由于 pretty-printer 限制了它的打印量（以减少大量输出），而不是 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)

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

Data Type in SMT solver which supports normal additon, xor, or , and operation simultaneously

python

jupyter-notebook

z3

smt

sat