z3 - z3的内存使用

Question

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

Answer 1

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

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

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