z3 - 是否应该施加额外的约束来缩短 SMT 求解器的求解时间？

Question

我有一个 SMT 应用程序(基于 Haskell SBV 库构建)，它针对单个 s 求解一些复杂的方程式使用 Z3 的实逻辑变量。就我而言，找到解决方案大约需要 30 秒。

为了加快速度，我添加了额外的约束 s < 40000 ，因为我对解决方案有一些估计。我在想这样的约束会缩小搜索空间并使求解器更快地返回结果。然而，这只会让它变慢(实际上它甚至没有在 10 分钟内完成)。

问题是:是否可以假设额外的约束条件总是会减慢/加快求解过程，或者没有通用规则并且总是视情况而定？

我担心即使我的 30 秒算法也可能包含一些不一定需要的额外约束，但只会减慢过程。

Answer 1

我认为您不能对此做出任何一般性假设。假设 sat/unsat 状态不变，它可能会也可能不会影响求解时间。

等式通常会有所帮助(因为它们可以自由传播)，但对于其他任何事情，这是任何人的猜测。此外，对于相同的加法，不同的求解器可能会表现出不同的行为。

考虑这一点的一种方法是，底层 DPLL(T) 算法本质上是一种非常智能的美化搜索算法。它不断产生“学习引理”，希望它能找到与先前已知事实的矛盾。您添加的新“约束”可能会导致它生成大量正确但不相关的引理，使它陷入困境而没有任何有用的结果。 (量化公式通常是这样的:您可以用一百万种不同的方式实例化它们；但除非您找到“正确”的实例化，否则它们所做的一切最终只会污染您的搜索空间。)

至少那是我的经历!