Z3 中恰好 n 编码

Question

我正在尝试在 Z3 的 UOD（此处为列表）中编码 'EXACTLY 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 中并不直接，因为变量是表达式，而不是类型值本身。所以我最初的尝试是编码 'At least N' 和 'At most N' 并将它们结合起来得到 'ExACTLY N'。改进最初的想法并使用我的逻辑 class 我将 'At most N' 替换为 (Not) 'At least 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 用户有一些很好的编码方法。谢谢。

Answer 1

您似乎需要伪布尔函数？ At-most/at-least/exactly 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

Z3 中恰好 n 编码

Exactly n encoding in Z3

python

logic

z3

z3py