增量求解如何在Z3中起作用？

Question

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

1. 有两种方法可以使用Z3进行增量求解:一种是推/弹(堆栈)模式,另一种是使用假设.Z3中的软/硬约束.
2. 在堆栈模式下,z3会忘记全局(我是对吗？)范围内所有学习的引理,即使在SMT求解器中有一个局部"弹出" 约束强化效率之后
3. 在假设模式中(我不知道名称,这是我想到的名称),z3不会简化一些公式,例如值传播.z3行为根据不满核心的要求而变化

我做了一些比较(欢迎你问一下这些公式,它们太大而无法放在rise4fun上),但这里是我的观察:在一些公式中,包括量词,假设模式更快.在一些包含大量布尔变量(假设变量)的公式中,堆栈模式比假设模式更快.

它们是否针对特定目的实施？增量求解如何在Z3中起作用？

Answer 1

是的,基本上有两种增量模式.

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

基于假设:使用传递给check()/ check_sat()的附加假设文字,您可以(1)在假设文字上提取不可满足的核心,(2)获得局部递增性,而无需独立于假设得到的垃圾收集引理.换句话说,如果Z3学习了一个不包含任何假设文字的引理,它就不会垃圾收集它们.要有效地使用假设文字,您还必须将它们添加到公式中.因此,权衡是与假设一起使用的子句包含一些膨胀.例如,如果要在本地假设某个公式(<= xy),则添加一个子句(=> p(<= xy)),并在调用check_sat()时假设为p.请注意,原始假设是一个单位.Z3有效地传播单位.使用假设文字的公式,它不再是搜索基础级别的单位.这会产生一些额外的开销.单位成为二元条款,二元条款成为三元条款等.

推送/弹出功能之间的区别适用于Z3的默认SMT引擎.这是大多数公式将使用的引擎.Z3包含一些引擎组合.例如,对于纯位传动问题,Z3可能最终使用基于sat的引擎.基于sat的引擎的增量实现与默认引擎不同.这里使用假设文字来实现增量.您在推送范围内添加的任何断言都被声明为隐含(=> scope_literals公式).这样的范围内的check_sat()必须处理假设文字.在翻盖侧,即不依赖于当前范围的任何后果(引理)是不是收集流行的垃圾().

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