如何提升Z3线性整数模理论SMT优化问题的求解速度？

我正在使用Z3的Python接口求解包含线性整数模理论（LIA）的SMT问题，场景类似Knuth所著《可满足性》一书第14页及后续章节的“学习布尔函数”示例。

我的问题包含数百个布尔公式，所有公式共享数十个待求解的整数变量与布尔变量，核心优化目标是最大化满足的公式数量。公式涉及混合布尔-整数约束，具体形式包括：

• x <= const（x为整数，const为常量）
• x1 + x2 <= const（x1、x2为整数）
• x == x1 + x2（x、x1、x2为整数）

已验证的优化手段 #

通过实验已确认以下有效提速方法：

• 使用z3.Solver()搭配二分法（反复求解目标函数≥给定阈值），比直接使用z3.Optimize()的求解速度快得多；
• 启用dt2bv策略可大幅提升求解效率。

但当前单个大型问题的求解时间仍长达数小时甚至数天，急需进一步优化。

Z3内置超100种策略及9000余项配置选项，但多数针对特定问题场景，恳请提供针对性的提速方向指引。如需示例运行的诊断输出，我可以随时提供。

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