1

我正在尝试使用 Z3 中的函数对公式进行编码，但我遇到了编码问题。考虑以下示例：

f(x) = x + 42
g(x1, x2) = f(x1) / f(x2)
h(x1, x2) = g(x1, x2) % g(x2, x1)
k(x1, x2, x3) = h(x1, x2) - h(x2, x3)
sat( k(y1, y2, y3) == 42 && k(y3, y2, y1) == 42 * 2 && ... )

我希望我的编码既高效（没有表达式重复）又允许 Z3 跨子问题重复使用有关函数的引理。这是我到目前为止所尝试的：

  1. 内联每个自由变量实例化 y1、y2 等的函数。这引入了重复，并且性能不如我希望的那么好。
  2. 用通用量词断言函数声明。这适用于非常具体的示例 - 从求解时间来看，Z3 似乎可以（？）重用涉及相同功能的先前查询的结果。但是，求解时间差异很大，并且在许多情况下 (1) 会更快。
  3. 使用函数定义（即量词+ MACRO_FINDER 选项）。如果我对文档的理解是正确的，这应该会扩展功能，因此应该接近（1）。然而，就性能而言，结果有点令人惊讶（“>”意味着更快）：
    • 对于 (1) > (2) 我得到的问题：(1) > (3) > (2)
    • 对于 (2) > (1) 的问题，我得到： (2) > (1) = (3)

我还尝试使用上述大部分内容调整 MBQI 选项（和其他选项）。但是，目前尚不清楚最佳组合是什么。我正在使用 Z3 4.0。

问题是：编码问题的“正确”方法是什么？请注意，我只有解释函数（我真的不需要 UF）。我可以使用这个事实进行更有效的编码并避免功能扩展吗？

谢谢

4

1 回答 1

1

我认为这个问题没有明确的答案。某些技术对一种类型的基准测试效果更好，而另一些技术对其他类型的基准测试效果更好。对于我们目前看到的 QBVF 基准，我们发现宏为我们提供了小基准规模和小求解时间的最佳组合，但这可能不适用于这种情况。

您对文档的理解是正确的，宏查找器将识别看起来像函数定义的量词，并用其定义替换对该函数的所有其他调用。可能并非所有宏都被拾取，或者您正在使用未正确检测到的准宏，这两种情况都可能有助于解释为什么性能有时比您的 (1) 更差。在 (1) > (3) 的情况下，差异有多大？预计会有一点开销，但运行时的巨大变化可能是由于某些宏格式错误或未被检测到。

一般来说，对这些问题进行编码并不是“正确”的方式。功能扩展并非总是可以避免的。权衡本质上是在急切地扩展 (1, 3) 或懒惰地扩展 (2) 之间。可能存在 SAT（快 1、3）和 UNSAT（快 2）类型的相关性，但也不能保证是这种情况。

于 2013-04-12T17:27:17.757 回答