Z3 中增量求解的工作原理是什么？答案

【问题标题】：How incremental solving works in Z3?Z3 中增量求解的工作原理是什么？
【发布时间】：2013-05-01 13:58:20
【问题描述】：

我有一个关于 Z3 如何逐步解决问题的问题。在这里阅读了一些答案后，我发现了以下内容：

使用Z3进行增量求解有两种方法：一种是push/pop(stack)模式，另一种是使用假设。 Soft/Hard constraints in Z3。
在堆栈模式下，z3 将忘记 global（我是对的吗？）范围内的所有学习引理，即使是在一个本地“pop”Efficiency of constraint strengthening in SMT solvers 之后
在假设模式下（我不知道名字，这是我想到的名字），z3 不会简化一些公式，例如价值传播。 z3 behaviour changing on request for unsat core

我做了一些比较（欢迎您询问公式，它们太大而无法放入rise4fun），但以下是我的观察：在某些公式上，包括量词，假设模式更快。在一些具有大量布尔变量（假设变量）的公式中，堆栈模式比假设模式更快。

它们是为特定目的而实施的吗？增量求解如何在 Z3 中工作？

【问题讨论】：

标签： z3 smt

【解决方案1】：

是的，基本上有两种增量模式。

基于堆栈：使用 push()、pop() 创建一个本地上下文，它遵循堆栈规则。在 push() 下添加的断言在匹配的 pop() 之后被删除。此外，任何在 push 下派生的引理都将被删除。使用 push()/pop() 模拟冻结状态并在冻结状态上添加附加约束，然后恢复到冻结状态。它的优点是释放了在 push() 范围内建立的任何额外内存开销（例如学习的引理）。工作假设是在推动下学习的引理将不再有用。

基于假设：使用传递给 check()/check_sat() 的附加假设文字，您可以 (1) 在假设文字上提取不可满足的核心，(2) 在不依赖于假设的垃圾收集引理的情况下获得局部增量。换句话说，如果 Z3 学习到一个不包含任何假设文字的引理，它预计不会对它们进行垃圾收集。要有效地使用假设文字，您也必须将它们添加到公式中。所以权衡是与假设一起使用的条款包含一些膨胀。例如，如果您想在本地假设某个公式 ( p (

push/pop 功能之间的区别适用于 Z3 的默认 SMT 引擎。这是大多数公式将使用的引擎。 Z3 包含一些引擎组合。例如，对于纯位向量问题，Z3 可能最终使用基于 sat 的引擎。基于 sat 的引擎中的增量与默认引擎的实现方式不同。这里增量是使用假设文字实现的。您在推送范围内添加的任何断言都被断言为暗示（=> scope_literals 公式）。 check_sat() 在这样的范围内将不得不处理假设文字。另一方面，任何不依赖于当前范围的结果（引理）不是在 pop() 上收集的垃圾。

在优化模式下，当您断言优化目标时，或者当您通过 API 使用优化对象时，您还可以调用 push/pop。不动点也是如此。对于这两个功能，push/pop 本质上是为了方便用户。没有内部增量。原因是这两种模式都使用了超非增量的大量预处理。

【讨论】：