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

【问题标题】：How to efficiently assert that two large sets don't intersect?如何有效地断言两个大集合不相交？
【发布时间】：2021-11-15 15:05:25
【问题描述】：

我有两个大型 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 之间的关系呈现给求解器，我担心这会损害性能。

【问题讨论】：

标签： z3 z3py

【解决方案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 求解器的工作变得困难。因此，您的里程可能会有所不同，具体取决于系统中的其他约束。）

对于任何与性能相关的东西，最好做一些实验，看看哪种效果最好。我认为这实际上取决于您对这些元素还有哪些其他限制以及这些新断言将如何与它们一起使用。在不知道您的整个约束集的情况下，这是任何人的猜测。

【讨论】：