我正在尝试使用Z3,将算术、量词和相等理论结合起来。但是这似乎并不是很有效,实际上,当可能时,用所有已实例化的基础实例替换量词似乎更加高效。考虑以下示例,在其中我已经对函数
生成这些公理需要0.002秒,然后在Z3中证明需要另外0.01秒(或更短时间)。当我们增加域中的对象或函数f的参数数量时,这个差异会迅速增加,并且量化的情况很快就变得不可行。
这让我想知道:当我们有一个有限的域时,为什么我们要首先在Z3中使用量词?我知道SMT使用启发式方法来寻找解决方案,但我感觉它仍然无法与特定于域的简单grounders竞争效率,后者将grounded实例提供给SMT,然后就成了SAT求解。我的直觉正确吗?
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求解。我的直觉正确吗?