在 Z3 中避免使用量词

Question

我正在试验 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 解决方案。我的直觉正确吗？

Answer 1

你的直觉是正确的。 Z3 中用于处理量词的启发式算法并未针对通用变量范围在有限/有界域上的问题进行调整。 在这类问题中，仅当需要极小比例的实例来表明问题不可满足时，才使用量词是一个不错的选择。

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

• Does Z3 take a longer time to give an unsat result compared to a sat result?

• 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 倍），求解扩展版本仍然更快。