52

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

  1. 使用Z3进行增量求解有两种方式：一种是push/pop(stack)模式，另一种是使用假设。Z3 中的软/硬约束。
  2. 在堆栈模式下，即使在一次局部“弹出”之后，z3 也会忘记全局（对吗？ ）范围内的所有学习引理SMT 求解器中约束加强的效率
  3. 在假设模式下（我不知道名字，这是我想到的名字），z3 不会​​简化一些公式，例如值传播。z3 行为根据 unsat 核心的请求而改变

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

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

4

1 回答 1

16

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

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

基于假设：使用传递给 check()/check_sat() 的附加假设文字，您可以（1）在假设文字上提取不可满足的核心，（2）在没有垃圾收集引理的情况下获得局部增量，而垃圾收集引理与假设无关。换句话说，如果 Z3 学习到一个不包含任何假设文字的引理，它预计不会对它们进行垃圾收集。要有效地使用假设文字，您也必须将它们添加到公式中。所以权衡是与假设一起使用的条款包含一些膨胀。例如，如果您想在本地假设某个公式 (<= xy)，则添加一个子句 (=> p (<= xy))，并在调用 check_sat() 时假设 p。请注意，最初的假设是一个单位。Z3 有效地传播单元。通过使用假设文字的公式，它不再是基本搜索级别的单位。这会产生一些额外的开销。单位变成二元从句，二元从句变成三元从句，等等。

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

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

于 2016-11-04T16:35:20.890 回答