Z3-Python中的SAT查询变慢了：增量式SAT怎么办？ [英] SAT queries are slowing down in Z3-Python: what about incremental SAT?
问题描述
在Z3(Python)中，循环内的SAT查询速度变慢，我可以使用增量SAT来解决此问题吗？
问题如下：我在循环中执行具体的SAT搜索。在每次迭代中，我都会得到一个模型(当然，我存储了该模型的否定，以便不会再次探索相同的模型)。此外，如果该模型满足某个属性，我还会添加它的子查询，并将其他限制添加到公式中。然后再次迭代，直到获得UNSAT(即不再有模型)。
我提供代码的定向快照：
...
s = Solver()
s.add(True)
while s.check() == sat:
s.check()
m = s.model()
phi = add_modelNegation(m)
s.add(phi) #in order not to explore the same model again
if holds_property(m): #if the model holds a property
s = add_moreConstraints(s,m) #add other constrains to the formula
...
问题是，随着s必须求解的公式变得越来越大，Z3开始有更多的困难来寻找这些模型。这没有关系：这应该会发生，因为现在由于添加了限制，查找模型变得更加困难。然而，在我的情况下，这种情况发生得太多了：计算速度甚至减半；即求解器需要在一些迭代后找到新模型的时间是以前的两倍。
因此，我想实现某种增量求解，并想知道Z3中是否有本机方法可以做到这一点。
我已经在很多页面上读到了这一点(例如，参见How incremental solving works in Z3?)，但只在How to use incremental solving with z3py中发现了这个响应：
PythonAPI是自动递增的。这只是意味着能够多次调用命令check()，而求解器不会忘记它以前看到的内容(即，调用check()，断言更多事实，再次调用check()；第二个check()将从一开始就考虑所有断言)。
我不确定我是否理解，因此我提出一个简单的问题：该响应是否意味着增量SAT确实在Z3的SAT中使用？我认为我正在寻找的点是另一个增量；例如：如果在SAT迭代编号230中，一个变量(比如说b1)是true是不可避免的，那么这是一个不会在之后改变的事实，您可以将其设置为1，简化公式，并且不对b1进行任何重新推理，因为如果有的话，所有的模型都将有b1。Z3的这个增量SAT是否考虑了这类情况？
如果不是，我如何实施此操作？
我知道在PySat或MiniSat中有一些实现，但我想在Z3中实现。
推荐答案
与任何与Z3解算性能相关的事情一样，没有一个统一的标准可以解决所有问题。每个具体问题都可以从不同的想法中受益。
增量求解术语在SAT/SMT上下文中有非常特定的含义。这意味着您可以在调用check之后继续向系统添加断言，而不会忘记之前添加的断言。这就是它递增的原因。此外，您还可以设置跳转点；也就是说，您可以告诉求解器忘记您在程序中某个点之后输入的断言，实质上是遍历一堆断言。有关详细信息，请参阅https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf的第3.9节，特别是其中介绍断言堆栈的部分。
而且，如前所述，您不必执行任何特定的操作即可使Z3递增。它默认是递增的，即调用check后可以简单地添加新的断言，或者使用push/pop调用等(对比一下，比如CVC4；默认情况下不是递增的。如果要在增量模式下使用CVC4，则必须传递特定的命令行参数。)这样做的主要原因是增量模式需要额外的簿记，除非您明确要求，否则CVC4不愿意为此买单。对于Z3，开发人员决定始终将其设置为增量，而不使用任何命令行开关。
b1为真会发生什么的特定问题：如果您以某种方式确定b1总是真的，只需断言它。求解器将自动利用这一点；不需要做任何特殊的事情。请注意，Z3在运行程序时会学习大量的词条，并将它们添加到其内部数据库中。但是，如果您有一些外部机制可以让您推导出特定的约束，那么只需添加它即可。(当然，这将取决于您，而不是Z3；但这是另一个问题。)在像您所做的那样加快枚举&Find Me All-Solution&qot；循环的过程中，有一个特定的诀窍是采用分而治之的方法，而不是添加先前模型的否定并迭代。在实践中，这可以在性能上产生显著的差异。我觉得你应该试试这个主意。如下所示：https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-blocking-evaluations如您所见，在该部分末尾定义的all_smt函数利用特定的增量(注意对push/pop的调用)来加速模型搜索过程，方法是仔细地将搜索空间划分为不相交的段，而不是执行随机漫游。使用此功能可能会给您带来所需的加速。但是，与任何特定于性能的方法一样，您需要更多地告诉我们您正在解决什么问题：这些方法都不能避免建模问题导致的性能问题。(例如，使用整数来模拟布尔值是一个常见的陷阱。)有关一般建议，请参阅以下答案：https://stackoverflow.com/a/57661441/936310
这篇关于Z3-Python中的SAT查询变慢了：增量式SAT怎么办？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
