3

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

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

问题是：是否可以假设附加约束总是减慢/加速求解过程，或者没有一般规则并且总是取决于情况？

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

4

1 回答 1

3

我认为您无法对此做出任何一般性假设。sat假设/unsat状态没有改变，它可能会或可能不会影响解决时间。

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

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

至少这是我的经验！

于 2019-02-13T21:22:22.130 回答