如何检查1000多个变量中没有重复值？

Question

我是 Z3 的新手，对于一个开源程序，我想使用 z3 求解器来提高效率。

我有大约 1000 多个

值

(declare-const a1 Int)
(declare-const a2 Int)
(declare-const a3 Int)
(declare-const a4 Int)
...

结果为

(declare-const x1 Int)
(declare-const x2 Int)
...
(assert (=  (+ a1 a2) x1) // in reality its not "plus" but more sophisticated
(assert (=  (+ a3 a4) x2) // however for simplicity lets keep it at that here.
...

现在我想确保所有 x1 到 x500+ 变量都有不同的值，并且没有重复项。

我当然可以

(assert (not (= x1 x2)))
(assert (not (= x1 x3)))
(assert (not (= x1 x4)))
...
(assert (not (= x2 x3)))
(assert (not (= x2 x4)))
...
(assert (not (= x718 719)))

这可行 - 但有更好的解决方案吗？

非常感谢！

Answer 1

您可以使用

distinct

（请参阅此示例）：

(assert (distinct x1 ... x500))

AFAIK，这通常在一系列不等式中内部扩展，就像您在示例中呈现的那样。

---

讨论：接下来是关于这种编码效率的纯理论讨论；

z3

是一个非常高效的 SMT 求解器，因此您可能不需要尝试比简单运行该工具更复杂的东西。

等式的否定（例如

(not (= x y))

）通常分为一对不等式：

x < y \/ x > y

假设

x < y

和

x > y

分别重命名为

B1

和

B2

，以下子句将被输入到 SAT 引擎：

B1 \/ B2

现在，考虑到您的问题，您会得到数百个这样的子句。这些在线性算术级别上都是相互关联的，但在 SAT 引擎运行的布尔级别上并不相关。因此，SAT 引擎可能会生成（大量）不一致的部分真值分配，这些分配通常违反

<

运算符的传递性属性，例如

 x < y /\ y < z /\ z < x

这些冲突将由 LRA 的理论求解器在“早期修剪”调用期间揭示，并通过学习阻止无效分配的冲突子句在布尔级别上解决。 你可以尝试什么：

如果你的问题承认这样的简化
• （如果

  x1 ... x500的名称可能被认为是完全任意的，之后可以对它们进行打乱..）

  ，你可能会得到更好的结果，对变量施加严格的总顺序

  x1 ... x500，例如 x1 < x2 /\ x2 < x3 /\ ... /\ x499 < x500

您可以尝试增加
• z3

  调用早期修剪的频率，如果这是一个可用的选项

  （注意：我不确定

  z3执行此类调用的频率）

您可以尝试

• mcSAT，它可以很好地应对这种限制。

---

编辑：

如果可以分配给变量

x_i

的值集是有限的并且在大小上有些限制，您可以尝试使用非标准

x_i

扩展来计算具有特定值的变量

z3

的数量来定义基数约束，例如

(assert
    ((_ at-most 1)
     (= x1 0)
     (= x2 0)
     ...
     (= x500 0)
    )
)
...
% repeat for all possible values 
...

我不确定此更改对性能的影响。在正常情况下，它会对性能产生积极影响，因为它会提前揭示冲突的分配（例如，参见

[1]

）。然而，您正在处理相当多的变量和变量的大量候选值x_i，因此在布尔级别上扁平化搜索可能有点过分了。