Z3 中的正好 n 编码答案

【问题标题】：Exactly n encoding in Z3Z3 中的正好 n 编码
【发布时间】：2017-12-08 06:19:21
【问题描述】：

我正在尝试在 Z3 的 UOD（此处为列表）中编码“完全 N”。我过去在 CBMC（C 有界模型检查器）中实现的方式是我将 List 定义为 _Bool 并使用无符号整数，并且只声明 B1 == N。

// L is the length of the List b1.
unsigned int B1 = 0
for i in range(L):
      B1 = b[i] + B1 
....
__CPROVER_assume (B1 == N);

在 Z3 中这并不简单，因为变量是表达式，而不是类型值本身。所以我最初的尝试是对“至少 N”和“最多 N”进行编码，并将它们结合起来得到“完全 N”。改进最初的想法并使用我的逻辑类，我将“最多 N”替换为（不）“至少 N+1”。但是对于 N >= 5 和 L =~ 600。代码在我的 4 Gb RAM 机器上耗尽内存。

# b1 is the List
X_list = []
for i in range(L-3):
  for j in range(i+1,L-2):
    l = And ( b1[j], b1[i])
    for k in range(j+1,L-1):
        l1 = And ( l, b1[k])
        for l in range(k+1,L):
            X_list.append( And (b1[l], l1))
B1 = Or(X_list)

File "file1.py", line 49, in <module> X_list.append( And (b1[l], l1)) File "/usr/lib/python2.7/dist-packages/z3/z3.py", line 1611, in And return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx) File "/usr/lib/python2.7/dist-packages/z3/z3core.py", line 1653, in Z3_mk_and raise Z3Exception(lib().Z3_get_error_msg(a0, err)) z3.z3types.Z3Exception: out of memory

有没有更好的方法在 Z3 中对此进行编码。也许经验丰富的 Z3 用户有一些很好的编码方式。谢谢。

【问题讨论】：

标签： python logic z3 z3py

【解决方案1】：

您似乎想要伪布尔函数？至多/至少/恰好 N 件事情是真的？可能还有系数？

如果是这样，Z3 通过 SMT-Lib 和各种 API 直接支持此功能。对于 Python，请参见此处：https://github.com/Z3Prover/z3/blob/b27a4a3593fd15c003d3e30da20b35ac96b7218e/src/api/python/z3/z3.py#L7718-L7793

对于 SMTLib，请参阅此处的讨论：K-out-of-N constraint in Z3Py

【讨论】：