4

我有一个关于量词的问题。

假设我有一个数组，我想为这个数组计算数组索引 0、1 和 2 -

(declare-const cpuA (Array Int Int))
(assert (or (= (select cpuA 0) 0) (= (select cpuA 0) 1))) 
(assert (or (= (select cpuA 1) 0) (= (select cpuA 1) 1))) 
(assert (or (= (select cpuA 2) 0) (= (select cpuA 2) 1)))

或者，我可以使用 forall 构造指定相同的 -

(assert (forall ((x Int)) (=> (and (>= x 0) (<= x 2)) (or (= (select cpuA x) 0) (= (select cpuA x) 1)))))

现在我想了解他们两个之间的区别。第一种方法执行速度很快，并给出了一个简单易读的模型。相比之下，第二个选项的代码量非常小，但程序需要时间来执行。而且解决方案也很复杂。

我想使用第二种方法，因为我的代码会变小。但是，我想找到一个可读的简单模型。

4

1 回答 1

4

量词推理通常非常昂贵。在您的示例中，量化公式等效于您提供的三个断言。但是，这不是 Z3 决定/解决您的公式的方式。Z3 使用称为基于模型的量词实例化 (MBQI) 的技术解决您的公式。这种技术可以决定许多片段（参见http://rise4fun.com/Z3/tutorial/guide）。它主要对本指南中描述的片段有效。它支持未解释的函数、算术和位向量理论。它还对数组和数据类型的支持有限。这足以解决您的示例。Z3 生成的模型似乎更复杂，因为使用相同的引擎来决定更复杂的片段。该模型应该看起来像一个小的功能程序。您可以在以下文章中找到有关此方法如何工作的更多信息：

请注意，数组理论主要用于表示/建模无界或大数组。也就是说，数组的实际大小未知或太大。所谓大，我的意思是公式中的数组访问次数（即selects）远小于数组的实际大小。我们应该问自己：“我们真的需要数组来建模/解决问题 X 吗？”。您可以考虑以下替代方案：

  • （未解释的）函数而不是数组。您的示例也可以编码为：

    (declare-fun cpuA (Int) Int)

    (assert (or (= (cpuA 0) 0) (= (cpuA 0) 1)))
    (assert (or (= (cpuA 1) 0) (= (cpuA 1) 1)))
    (assert (or (= (cpuA 2) 0) (= (cpuA 2) 1)))

  • 程序化 API。我们已经看到了许多使用数组（和函数）来提供紧凑编码的示例。紧凑而优雅的编码不一定更容易解决。实际上，通常情况正好相反。您可以使用 Z3 的编程 API 实现两全其美（性能和紧凑性）。在以下链接中，我为“数组”的每个位置使用一个“变量”对您的示例进行了编码。宏/函数用于编码约束，例如：表达式是 a0或1。 http://rise4fun.com/Z3Py/JF

于 2012-04-05T21:02:33.260 回答