z3求解MILP时效率远低于CBC的原因与优化方法

z3求解纯MILP问题的效率远低于CBC是非常普遍的情况，不存在反常的配置错误，核心原因有两点：

• z3的设计定位本就不是高性能纯MILP求解
  z3是通用满足性模理论（SMT）求解器，内置的整数线性规划模块是为整个SMT框架服务的，没有针对纯线性整数规划场景做深度优化。CBC是专门的开源MILP求解器，内置了经过十余年迭代的割平面生成、分支策略、节点剪枝、整数松弛热启动等全套优化逻辑，同等问题规模下比z3快1-2个数量级是正常表现。
• 确实存在可优化的z3配置项，但这些配置最多缩小部分效率差距，无法追平专业MILP求解器的性能
  对z3的MILP求解场景，可调整的常规优化配置包括：
  • 为所有整数变量设置明确、紧致的上下界，避免z3在无界整数域上盲目搜索
  • 显式指定求解器仅启用线性整数规划理论模块，关闭其他用不到的理论（如非线性运算、位向量、数组逻辑等），减少求解器的冗余开销
  • 开启auto_config参数，让z3自动匹配问题类型调整搜索策略，避免默认使用通用SMT的保守搜索配置
    即便完成所有上述优化，z3求解纯线性MILP的速度也很难达到CBC的水平，跑半小时仍无结果的情况属于正常表现，并非你的使用错误。

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