如何有效地断言两个大集合不相交？

Question

我有两个大型 Z3 整数变量集合。将它们称为集合 A 和集合 B。（预先知道组成员身份，因此无需使用 Z3 集。）我需要生成断言以确保 A 中的元素不等于 中的元素B.显而易见的方法如下：

for all a in A:
  for all b in B:
    solver.add(a != b);

但是，集合很大，这将增加超过 2000 万个断言，因此这不是一个选项。

这是我想出的另一种方法，它只涉及断言总共 O(n+m) 个子句：

a = ctx.int_const("a");
a_def = (a == A[0] || a == A[1] || ... || A[n]);

b = ctx.int_const("b");
b_def = (b == B[0] || b == B[1] || ... || B[m]);

solver.add(z3::forall(a, b, z3::implies(a_def && b_def, a != b)));

有没有更有效的方法来做到这一点？似乎上述方法以间接方式向求解器呈现 A 和 B 之间的关系，我担心这会损害性能。

Answer 1

我认为你最好的选择是直接使用 Distinct (https://z3prover.github.io/api/html/namespacez3py.html#a9eae89dd394c71948e36b5b01a7f3cd0):

s.add(Distinct(*(A+B)))

并且 z3 将在内部使用伪布尔编码处理此问题（希望如此！）并且非常高效。请注意，这只是一个子句，尽管在内部 z3 会将其转换为一种有效的形式。

由于您已经假设 A 和 B 是集合，因此另一种选择是使用 min(m,n) 调用 Distinct:

for a in A:
    s.add(Distinct(a, *B))

显然，在较短的列表上执行此循环；从而创建 min(m,n) 个断言。

您的 O(m+n) 解决方案也可以很好地工作。我没有看到任何不应该这样做的明显原因。（尽管量词的存在让 SMT 求解器的日子不好过。因此，您的里程数可能会有所不同，具体取决于系统中的其他约束。）

对于任何与性能相关的内容，最好进行一些实验，看看哪种效果最好。我认为这实际上取决于您对这些元素还有哪些其他约束以及这些新断言与它们的配合情况。在不知道整个约束集的情况下，任何人都可以猜测。

如何有效地断言两个大集合不相交？

How to efficiently assert that two large sets don't intersect?

z3

z3py