9

我正在试验 Z3，我结合了算术、量词和相等的理论。这似乎不是很有效，事实上，在可能的情况下用所有实例化的地面实例替换量词似乎更有效。考虑以下示例，其中我为一个函数编码了唯一名称公理，该函数f接受两个 sort 参数Obj并返回一个解释的 sort 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 解决方案。我的直觉正确吗？

4

1 回答 1

7

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

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

这是代码片段之一：

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

于 2012-11-07T14:42:55.003 回答