避免在 Z3 中使用量词 [英] Avoiding quantifiers in Z3
问题描述
我正在试验 Z3，我结合了算术、量词和等式的理论.这似乎不是很有效，事实上，在可能的情况下，用所有实例化的地面实例替换量词似乎更有效.考虑以下示例，其中我对函数 f 的唯一名称公理进行了编码，该函数接受两个排序 Obj 参数并返回一个已解释的排序 S.这个公理指出 f 的每个唯一参数列表都返回一个唯一对象:
I am experimenting with Z3 where I combine the theories of arithmetic, quantifiers and equality. This does not seem to be very efficient, in fact it seems to be more efficient to replace the quantifiers with all instantiated ground instances when possible. Consider the following example, in which I have encoded the unique names axiom for a function f that takes two arguments of sort Obj and returns an interpreted sort S. This axiom states that each unique list of arguments to f returns a unique object:
(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 量词实例化来证明这一点.当我编写一个生成此公式实例的简单脚本时:
Although this is a standard way of defining such an axiom in logic, implementing it like this is computationally very expensive. It contains 4 quantified variables, which each can have 8 values. This means that this results in 8^4 = 4096 equalities. It takes Z3 0.69s and 2016 quantifier instantiations to prove this. When I write a simple script that generates the instances of this formula:
(assert (distinct (f o1 o1) (f o1 o2) .... (f o8 o7) (f o8 o8)))
生成这些公理需要 0.002 秒，而在 Z3 中又需要 0.01 秒(或更少)来证明它.当我们增加域中的对象或函数 f 的参数数量时，这种差异会迅速增加，并且量化的情况很快变得不可行.
It takes 0.002s to generate these axioms, and another 0.01s (or less) to prove it in Z3. When we increase the objects in the domain, or the number of arguments to the function f this different increases rapidly, and the quantified case quickly becomes unfeasible.
这让我想知道:当我们有一个有界域时，为什么我们首先要在 Z3 中使用量词?我知道 SMT 使用启发式方法来寻找解决方案，但我觉得它仍然无法与将接地实例提供给 SMT 的简单的特定于领域的接地器在效率上竞争，这只不过是 SAT 求解.我的直觉正确吗?
This makes me wonder: when we have a bounded domain, why would we use quantifiers in Z3 in the first place? I know that SMT uses heuristics to find solutions, but I get the feeling that it still cannot compete in efficiency with a simple domain-specific grounder that feeds the grounded instances to SMT, which is then nothing more than SAT solving. Is my intuition correct?
推荐答案
你的直觉是正确的.用于处理 Z3 中的量词的启发式方法未针对通用变量范围在有限/有界域上的问题进行调整.在这类问题中，仅当需要非常少的实例来表明问题不可满足时，才使用量词是一个不错的选择.
Your intuition is correct. The heuristics for handling quantifiers in Z3 are not tuned for problems where universal variables range over finite/bounded domains. In this kind of problem, using quantifiers is a good option only if a very small percentage of the instances are needed to show that a problem is unsatisfiable.
我通常建议用户使用程序化 API 扩展这个量词.这里有两个相关的帖子.它们包含指向实现此方法的 Python 代码的链接.
I usually suggest that users should expand this quantifiers using the programmatic API. Here a two related posts. They contain links to Python code that implements this approach.
这是其中一段代码:
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.
In this example, I'm essentially encoding 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 次)，解决扩展版本仍然更快.
Finally, your encoding (assert (distinct (f o1 o1) (f o1 o2) .... (f o8 o7) (f o8 o8)) is way more compact than expanding the quantifier 4096 times. However, even if we use a naive encoding (just expand the quantifier 4096 times), it is stil faster to solve the expanded version.
这篇关于避免在 Z3 中使用量词的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
