2

一般问题

我已经多次注意到push-pop已经弹出的范围似乎会影响check-sat后续范围中的 a 所需的时间。

也就是说，假设一个程序具有多个（可能是任意嵌套的）push-pop 作用域，每个作用域都包含一个 check-sat 命令。此外，假设第二个 check-sat 需要 10 秒，而第一个只需要 0.1 秒。

...
(push)
  (assert (not P))
  (check-sat) ; Could be sat, unsat or unknown
(pop)
...
(push)
  (assert (not Q))
  (check-sat) ; Could be sat, unsat or unknown
(pop)

注释完第一个 push-pop 范围后，第二个 check-sat 只需要 1s。这是为什么？

  • AFAIK，如果使用推弹范围，Z3 会切换到增量求解器。他们为什么会这样表现有（概念上的）原因吗？

  • 曾经有人告诉我，Z3 按重要性为符号分配属性，这会影响证明搜索（在证明搜索期间，符号的重要性也会发生变化）。这可能是原因吗？是否可以重置重要性（在范围之间）？

  • 这可能是一个错误吗？我发现这篇文章Leonardo 提到了一个似乎相关的错误（不过，他的回答来自 2012 年）。

具体实例

不幸的是，我只有相当长的（自动生成的）SMTLib 文件来说明该行为，您可以在此 gist中找到其中一个文件。它使用量词和未解释的函数，但既不使用mbqi数组也不使用位向量。该示例由 148 个嵌套的 push-pop 作用域和 89 个 check-sat 组成，Z3 4.3.2 大约需要 8s 来处理它。最后一次检查（以 为前缀echo）耗时最长。

我随机评论了几个 push-pop 作用域（一次一个，永远不会是最后一个，确保你没有评论符号声明），并且在大多数情况下，整体运行时间下降到不到 1 秒。也就是说，最后一次检查坐的速度要快得多。

为了提供更多详细信息，我将运行 Z3 与所有范围（慢，8 秒）与运行 Z3 进行比较，其中标记的范围[XXX]已被注释（快速，0.3 秒）。结果可以在这个差异中看到（左慢，右快）。

diff 表明所有检查-sat 的行为都相同（我通过回显“unsat”来伪造评论过的一个），从中我得出结论，评论范围会影响证明搜索，但不会影响其最终结果。

我还试图从获得的统计数据的差异中找出一些意义，但我对如何正确解释统计数据知之甚少。以下是我能理解的一些统计数据：

  • grobner（383 vs 36）和nonlinear-horner（342 vs 25），所以看起来较慢的运行执行更多与算术相关的操作。注释范围确实即将进行非线性算术（许多其他算法也是如此），但是注释范围中的特定证明应该是“微不足道的”，它本质上表明x != 0对于x已0 < x明确假设的一个。

  • memory（40 vs 7），我解释为表明Z3在程序的慢版本中探索了更大的搜索空间

  • quant-instantiations（43k vs 51k），这让我感到惊讶，因为明显更快的运行仍然触发了更多的量词实例化。

4

1 回答 1

4

我不确定这是观察还是问题？是的，Z3 对于不同的输入会有不同的表现，并且 push/pop 不是“无辜的”，即它们会对性能产生重大影响。如果可以完全删除它们，这一点最为明显，因为这允许 Z3 切换到完全不同的不支持增量的子求解器（但通常更快）。例如，对于没有作用域的纯位爆破公式，Z3 将使用一个快速的新 SAT 求解器，但如果需要推送/弹出，它会回退到一个更老、更慢的 SAT 求解器（这两个求解器的实现完全不相交）。

此外，删除其他范围之间的一些范围也可能产生巨大影响，因为它允许 Z3 保留更多中间引理以及启发式状态。如果出于某种原因希望每个查询都表现得好像没有其他查询一样，那么最好简单地生成独立的查询并在每个查询上从头开始启动 Z3。

有关提到的具体问题的更多信息：

“启发式状态”是指 Z3 使用的各种启发式数据，有大量不同的启发式在工作，而不仅仅是一个特定的启发式，比如符号排序。在查询之间保留此信息是否“好”完全取决于您的问题 - 启发式方法适用于某些问题，但并非全部适用，就像启发式方法的本质一样。但是，增量的整个概念都建立在此之上：如果启发式方法没有帮助，那么我们最好运行独立查询。但是，在某些应用程序中，有时重置 Z3比不重置或独立查询要好，例如，当您有大量微小查询时。

切换到不同求解器的概念原因：第一个不支持您需要的功能。参见combine_solver.cpp，函数check_sat。如果未使用solver1（例如，如果提供假设或启用增量模式），则将使用solver2。

combined_solver.solver2_timeout将放置一个超时求解器2。选项设置求解器 2 超时时会发生什么combined_solver.solver2_unknown。所以，是的，你可以在solver2 之后运行solver1，但是也允许solver1 失败，即返回unknown。查看代码，如果使用它可能是不合理的（例如，忽略假设）。

回复：提到的错误报告：那是一个健全性错误，而不是性能错误；其中一个求解器说 SAT，另一个说 UNSAT。

于 2015-01-20T14:39:12.263 回答