z3 - 输入顺序对约束求解器性能的影响

Question

输入（布尔和算术方程）顺序对 Gecode 等约束求解器和 Microsoft Z3 等 SMT 求解器是否重要？如果是，如果我可以利用 Gecode 中的分支功能利用一些已知的启发式方法，这两者中的哪一个会表现得更好？

（注：我不知道Gecode中类似branch()的函数是否存在于Z3中）

Answer 1

理论上，没有；顺序应该无关紧要。断言的顺序不应该有所作为。但在实践中，它们可能会产生影响，因为启发式方法最终可能会在死胡同中花费大量时间。SMT 求解器通常作为黑盒工作，也就是说，除非您知道它们的确切内部结构，否则很难看到它们的进展情况。但是，您可以调高详细程度（使用 z3 的-v标志）并可能查看输出以查看是否发现任何不同的行为。

与任何一般的“SMT 求解器性能”问题一样，不可能抽象地回答。每个问题实例都有特定的特征，并且可能有不同的编码方式以使求解器更容易。如果您发布特定问题，您可以获得更好的建议。