Z3中的所有其他约束

Question

是否有一种方法可以在仅使用O（n）语句的Z3中生成所有除例外的约束？我知道XCSP3提供了此功能。

目前可以使用O（n ^ 2）语句来完成：

for i in range(len(G) - 1):
    s.add( [ Or(G[i] == 0, G[i] != G[j]) for j in range(i + 1, len(G)) ] )

如果重要，我有兴趣比较位向量。

Answer 1

Z3确实带有Distinct谓词，该谓词可确保所有元素都是不同的，但据我所知，没有内置distinct-except。

假设您的元素列表足够小（可以说<20个），我认为您真的无法以任何可衡量的方式击败二次扩展。如果您确实有大量元素，那么我会采用一种略有不同的方法，即使用数组来跟踪插入的元素。像这样的东西：

from z3 import *

def distinct_except(s, ignored, G):
   if not G:
       return BoolSort().cast(True)

   A   = K(G[0].sort(), False);
   res = True

   for i in range(len(G)):
       isIgnored = G[i] == ignored
       res = If(isIgnored, res, And(res, Not(A[G[i]])))
       A   = If(isIgnored, A,   Store(A, G[i], True))

   return res

我们只构建了两个并行表达式，一个是数组A，其中包含您要检查的所有元素，这些元素不会被忽略。第二个是变量res，它简单地跟踪我们要插入的元素是否已在数组中。

这将使表达式res和A的大小保持线性，并且z3应该能够相当有效地处理它。如果您发现其他情况，我想听听。

这里有一些测试可以看到它的实际效果：

# Test: Create four variables, assert they are distinct in the above sense
a, b, c, d = BitVecs('a b c d', 32)
s = Solver()
s.add(distinct_except(s, 0, [a, b, c, d]))

# Clearly sat:
print s.check()
print s.model()

# Let's get a slightly more interesting model, make c 5:
s.add(c == 5)
print s.check()
print s.model()

# Add a constraint that a and b are equal
# Still SAT, because we can make a and b 0
s.add(a == b)
print s.check()
print s.model()

# Force a to be non-zero
s.add(a != 0)

# Now we have unsat:
print s.check()

此打印：

sat
[c = 0, b = 0, d = 2, a = 0]
sat
[b = 0, a = 0, d = 1, c = 5]
sat
[b = 0, a = 0, d = 1, c = 5]
unsat

请注意，在调用print s.sexpr()来查看它们随着输入列表变大时如何增长之前，可以始终使用s.check()来查看所生成的表达式。