避免在Z3中使用量词

Question

避免在Z3中使用量词

9

我正在尝试使用Z3，将算术、量词和相等理论结合起来。但是这似乎并不是很有效，实际上，当可能时，用所有已实例化的基础实例替换量词似乎更加高效。考虑以下示例，在其中我已经对函数 f 进行了唯一命名公理的编码，该函数需要两个类型为Obj的参数，并返回解释类型S。此公理指出，每个唯一的参数列表都将返回一个唯一的对象：

(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.69秒和2016个量化实例。当我编写一个简单的脚本来生成此公式的实例时：

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

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

这让我想知道：当我们有一个有限的域时，为什么我们要首先在Z3中使用量词？我知道SMT使用启发式方法来寻找解决方案，但我感觉它仍然无法与特定于域的简单grounders竞争效率，后者将grounded实例提供给SMT，然后就成了SAT求解。我的直觉正确吗？

- marczoid

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Leonardo de Moura · Accepted Answer

您的直觉是正确的。在 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次），解决展开版本仍然更快。