Z3 中增量求解的工作原理是啥?
Posted
技术标签:
【中文标题】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 中工作?
【问题讨论】:
【参考方案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 本质上是为了方便用户。没有内部增量。原因是这两种模式都使用了超非增量的大量预处理。
【讨论】:
以上是关于Z3 中增量求解的工作原理是啥?的主要内容,如果未能解决你的问题,请参考以下文章