z3 - z3的内存使用情况

Question

我正在使用 z3 来解决线性混合自动机的可达性问题。我在有限的内存下运行实验。我对内存使用感到困惑。有一种情况，z3在给定bound 2500的有限内存下可以解决。但是，当bound设置为2000时，z3的内存使用量超过了最大允许，这是什么原因呢？

Answer 1

SMT2文件中的约束数量较少并不一定意味着Z3会使用较少的内存来解决问题。例如，一个小但无法满足的问题可能比一个大的可满足问题需要更多的内存。

设置自动机展开的下限很可能会将可满足的问题（在边界 2500）变成不可满足的问题（在边界 2000），这反过来又使 Z3 的问题变得更加困难，即使更少约束。因此，Z3 将使用更多的时间和/或内存。

解决这个问题可能需要对问题进行不同的编码或在求解器上使用不同的选项，例如，调整启发式算法，使它们更频繁地“幸运”并更早地找到解决方案。