scope - 为什么已经弹出的作用域会影响后续作用域中的 check-sat 时间？

Question

一般问题

我多次注意到 push-pop已经弹出的范围似乎会影响 check-sat 的时间在随后的范围内需要。

也就是说，假设一个程序具有多个(可能是任意嵌套的)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。这是为什么？

• 据我所知，如果使用 push-pop 示波器，Z3 会切换到增量求解器。是否有(概念上的)原因可以解释为什么他们会这样做？

• 有人告诉我，Z3 按重要性给符号赋予属性，这会影响证明搜索(而且符号的重要性也会在证明搜索期间发生变化)。这可能是原因吗？是否可以重置重要性(在范围之间)？

• 会不会是一个错误？我找到了 this post莱昂纳多提到了一个似乎相关的错误(不过他的回答是从 2012 年开始的)。

具体实例

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

我随机注释了几个 push-pop 作用域(一次一个，绝不是最后一个，确保你没有注释符号声明)，在大多数情况下，整体运行时间下降到不到 1 秒。也就是说，最后一次 check-sat 的完成速度要快得多。

为了提供更多细节，我比较了所有范围(慢，8 秒)的 Z3 运行和范围标记为 [XXX] 的 Z3 运行。已被评论(快，0.3 秒)。结果可见this diff (左边慢，右边快)。

diff 显示所有 check-sats 的行为都相同(我通过回显“unsat”伪造了评论的结果)，从中我得出结论，评论的范围会影响证明搜索，但不会影响其最终结果。

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

• grobner (383 比 36)和 nonlinear-horner (342 对 25)，所以看起来较慢的运行执行更多与算术相关的操作。注释范围确实是关于非线性算术的(还有很多其他的)，但注释范围内的特定证明应该是“微不足道的”，它本质上表明 x != 0对于 x关于哪个0 < x已明确假定。

• memory (40 vs 7)，我认为这表明 Z3 在程序的慢版本中探索了更大的搜索空间

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

Answer 1

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

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

关于所提到的具体问题的更多信息:

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

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

combined_solver.solver2_timeout 将放置一个超时 solver2。当 solver2 超时时会发生什么情况由选项 combined_solver.solver2_unknown 设置。所以，是的，您可以在 solver2 之后运行 solver1，但也允许 solver1 失败，即返回未知。查看代码，如果使用它，它很可能是不可靠的(例如，忽略假设)。

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