Z3 中的增量求解如何工作? [英] How incremental solving works in Z3?

问题描述

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

I have a question regarding how Z3 incrementally solves problems. After reading through some answers here, I found the following:

1. 使用 Z3 进行增量求解有两种方法:一种是 push/pop(stack) 模式，另一种是使用假设.Z3 中的软/硬约束.
2. 在堆栈模式下，即使在一个本地弹出"SMT 求解器中约束强化的效率
3. 在假设模式下(我不知道名字，这是我想到的名字)，z3 不会​​简化一些公式，例如价值传播.z3 行为根据 unsat 核心请求而改变

我做了一些比较(欢迎你索取公式，它们太大了，不能放在rise4fun上)，但这是我的观察:在一些公式上，包括量词，假设模式更快.在一些包含大量布尔变量(假设变量)的公式上，堆栈模式比假设模式更快.

I did some comparison (you are welcome to ask for the formulas, they are just too large to put on the rise4fun), but here are my observations: On some formulas, including quantifiers, the assumptions mode is faster. On some formulas with lots of boolean variables (assumptions variables), stack mode is faster than assumptions mode.

它们是否出于特定目的而实施?Z3 中的增量求解如何工作?

Are they implemented for specific purposes? How does incremental solving work in Z3?

推荐答案

是的，本质上有两种增量模式.

Yes, there are essentially two incremental modes.

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

Stack based: using push(), pop() you create a local context, that follows a stack discipline. Assertions added under a push() are removed after a matching pop(). Furthermore, any lemmas that are derived under a push are removed. Use push()/pop() to emulate freezing a state and adding additional constraints over the frozen state, then resume to the frozen state. It has the advantage that any additional memory overhead (such as learned lemmas) built up within the scope of a push() is released. The working assumption is that learned lemmas under a push would not be useful any longer.

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

Assumption based: using additional assumption literals passed to check()/check_sat() you can (1) extract unsatisfiable cores over the assumption literals, (2) gain local incrementality without garbage collecting lemmas that get derived independently of the assumptions. In other words, if Z3 learns a lemma that does not contain any of the assumption literals it expects to not garbage collect them. To use assumption literals effectively, you would have to add them to formulas too. So the tradeoff is that clauses used with assumptions contain some amount of bloat. For example if you want to locally assume some formula (<= x y), then you add a clause (=> p (<= x y)), and assume p when calling check_sat(). Note that the original assumption was a unit. Z3 propagates units efficiently. With the formulation that uses assumption literals it is no longer a unit at the base level of search. This incurs some extra overhead. Units become binary clauses, binary clauses become ternary clauses, etc.

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

The differentiation between push/pop functionality holds for Z3's default SMT engine. This is the engine most formulas will be using. Z3 contains some portfolio of engines. For example, for pure bit-vector problems, Z3 may end up using the sat based engine. Incrementality in the sat based engine is implemented differently from the default engine. Here incrementality is implemented using assumption literals. Any assertion you add within the scope of a push is asserted as an implication (=> scope_literals formula). check_sat() within such a scope will have to deal with assumption literals. On the flip-side, any consequence (lemma) that does not depend on the current scope is not garbage collected on pop().

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

In optimization mode, when you assert optimization objectives, or when you use the optimization objects over the API, you can also invoke push/pop. Likewise with fixedpoints. For these two features, push/pop are essentially for user-convenience. There is no internal incrementality. The reason is that these two modes use substantial pre-processing that is super non-incremental.

这篇关于Z3 中的增量求解如何工作?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！