避免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.002s,而在Z3中需要0.01s(或更少).当我们增加域中的对象或函数的参数数量时,f这种差异会迅速增加,并且量化的情况很快变得不可行.

这让我想知道:当我们有一个有界域时,为什么我们首先在Z3中使用量词？我知道SMT使用启发式方法来寻找解决方案,但我感觉它仍然无法与一个简单的特定于域的地面实施竞争,后者将基础实例提供给SMT,这仅仅是SAT解决方案.我的直觉是否正确？

Answer 1

你的直觉是正确的.在Z3中处理量词的启发式方法并未针对通用变量超出有限/有界域的问题进行调整.在这种问题中,只有在需要很小比例的实例来表明问题不可满足时,才使用量词是一个很好的选择.

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

• 与sat结果相比,Z3是否需要更长的时间才能得到不满的结果？

• 量词与非量词

这是代码片段之一:

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次),解决扩展版本也会更快.