Python Z3约束添加顺序优化求解速度：相等约束是否应优先添加

结论 #

相等约束应该优先于所有复杂约束提前添加，和你预期的逻辑一致，s.add(x == y)这类相等约束越靠前放，求解提速效果越明显。

原因说明 #

• Z3求解器内置的等价类推理逻辑优先级很高，前置添加的相等约束会被求解器先捕获，生成变量等价关系表，后续再添加复杂约束时，求解器会自动用等价关系替换约束中的变量，直接减少复杂约束的自由变量数量，大幅降低后续约束的处理复杂度。
• 相等约束本身的校验成本极低，提前完成相等约束的校验后，会直接剪掉完全不符合等价条件的解空间，后续check()阶段遍历可行解的范围会被提前压缩，不需要到处理复杂约束的时候再做无效的分支判断。
• 针对你嵌套循环生成大量约束的场景，前置相等约束的收益会被放大：每一轮循环生成的复杂约束都会自动应用已经确定的等价关系做化简，不会出现大量冗余的约束表达式。

代码调整建议 #

你可以调整代码逻辑，把所有静态可确定的相等约束、变量赋值类约束先全部批量添加到Solver实例后，再执行嵌套循环添加复杂约束的逻辑即可。

内容的提问来源于stack exchange，提问作者user8922738