Z3:断言约束的顺序是否影响它们被评估的顺序?

Question

我的z3py代码正在进行推理，遇到了一些性能(延迟)问题。目前，我正在尝试提出一些启发式方法来精简搜索空间，希望能提高推理速度。

我的问题是:被断言的约束的顺序是否影响它们被评估的顺序?换句话说，如果一个约束可以显著减少搜索空间，我是否应该首先断言它，以便在评估之后，在早期阶段排除许多不可能的解决方案?

Answer 1

断言的顺序可以对稍后的启发式产生影响，但是没有预先定义的执行"最佳"的顺序。一般来说，更早地断言特定的约束并不意味着它们将首先得到解决。