避免 Z3 中的量词

我正在尝试 Z3，其中结合了算术、量词和等式的理论。这似乎不是很有效，事实上，在可能的情况下用所有实例化的基础实例替换量词似乎更有效。考虑以下示例，其中我对函数的唯一名称公理进行了编码f需要两个参数Obj并返回解释的排序S。该公理指出，每个唯一的参数列表f返回一个唯一的对象：

(declare-datatypes () ((Obj o1 o2 o3 o4 o5 o6 o7 o8)))
(declare-sort S 0)

(declare-fun f (Obj Obj) S)
(assert (forall ((o11 Obj) (o12 Obj) (o21 Obj) (o22 Obj))
    (=> 
        (not (and (= o11 o21) (= o12 o22)))
        (not (= (f o11 o12) (f o21 o22))))))

尽管这是在逻辑中定义此类公理的标准方法，但像这样实现它在计算上非常昂贵。它包含 4 个量化变量，每个变量可以有 8 个值。这意味着这会导致8^4 = 4096平等。需要 Z3 0.69s 和 2016 量词实例化来证明这一点。当我编写一个生成此公式的实例的简单脚本时：

(assert (distinct (f o1 o1) (f o1 o2) .... (f o8 o7) (f o8 o8)))

生成这些公理需要 0.002 秒，在 Z3 中证明它还需要 0.01 秒（或更短）。当我们增加域中的对象或函数的参数数量时f这种差异迅速增加，量化的情况很快变得不可行。

这让我想知道：当我们有一个有界域时，为什么我们首先要在 Z3 中使用量词？我知道 SMT 使用启发式方法来寻找解决方案，但我感觉它在效率上仍然无法与将接地实例提供给 SMT 的简单特定领域接地器竞争，而这只不过是 SAT 求解。我的直觉正确吗？

你的直觉是正确的。 Z3 中处理量词的启发式方法不适用于通用变量范围超过有限/有界域的问题。 在此类问题中，仅当需要很小比例的实例来表明问题不可满足时，使用量词才是一个不错的选择。

我通常建议用户使用编程 API 来扩展这个量词。 这里有两个相关的帖子。它们包含实现此方法的 Python 代码的链接。

• 与满意的结果相比，Z3 是否需要更长的时间才能给出不满意的结果？ https://stackoverflow.com/questions/12659098/does-z3-take-a-longer-time-to-give-an-unsat-result-compared-to-a-sat-result

• 量词与非量词 https://stackoverflow.com/questions/10011478/quantifier-vs-non-quantifier

这是代码片段之一：

VFunctionAt = Function('VFunctionAt', IntSort(), IntSort(), IntSort())

s = Solver()
s.add([VFunctionAt(V,S) >= 0 for V in range(1, 5) for S in range(1, 9)])
print s

在这个例子中，我本质上是在编码forall V in [1,4] S in [1,8] VFunctionAt(V,S) >= 0.

最后，你的编码(assert (distinct (f o1 o1) (f o1 o2) .... (f o8 o7) (f o8 o8))比将量词扩展 4096 倍要紧凑得多。然而，即使我们使用简单的编码（只需将量词扩展 4096 倍），解决扩展版本的速度仍然更快。