我有一个SMT应用程序（建立在Haskell SBV库上），它使用Z3解决了在Real逻辑中针对单个s变量的一些复杂方程。在我的案例中，寻找解决方案大约需要30秒。
为了加快速度，我添加了额外的约束s < 40000，因为我有一些解决方案的估计。我认为这样的约束会缩小搜索空间并使求解器更快地返回结果。然而，这只会让它变慢（实际上甚至没有在10分钟内完成）。
问题是：是否可以假设额外的约束总是减慢/加速解决方案流程，或者没有一般规则并且它总是取决于具体情况？
我担心即使我的30秒算法可能包含一些不一定需要的额外约束，但只会减慢过程。