Z3求解简单ILP最大化问题时返回正无穷结果异常咨询

Z3返回正无穷的结果是符合逻辑的，核心问题是你混淆了整数线性规划的建模约定和SMT求解器的默认规则：

• SMT-LIB中声明的Int类型变量取值范围是全体整数，包含负整数，不存在"变量默认非负"的隐含约束。你提到的"ILP变量非负"是建模者需要手动添加的业务约束，不会被Z3自动生效。
• 你写的第一个问题的约束没有对x1、x2的取值做下界限制，导致目标函数不存在上界，自然会返回正无穷。

把你第一个问题的约束代入目标函数做化简就能看得很清楚：

1. 固定约束：x0=1，x1+x2=x0=1，x3=x1+x2=1
2. 代入目标函数：

   5*x0 +10*x1 +6*x2 +9*x3
   = 5*1 + 10x1 +6x2 +9*1
   = 14 + 10x1 +6x2
   

3. 结合约束x2 = 1 - x1，进一步化简目标为20 + 4*x1
4. 因为你没有加x1 >=0、x2 >=0的约束，x1可以取任意大的正整数（此时x2取对应的负整数即可满足x1+x2=1的约束），x1越大目标值越高，没有上限，因此Z3判定目标值为正无穷。

你看到的输出里的模型（x1=1、x2=0）只是Z3找到的任意一个可行解，不是最优解——当问题不存在有限最优解时，Z3只会返回一个满足约束的样例，不会做最优性保证。

第二个问题里你手动给变量加了有上界的约束：

• (assert (< x 2))在整数域等价于x ≤1
• (assert (< (- y x) 1))在整数域等价于y ≤x
  两个变量都被约束了上界，目标函数x+y不存在无限增大的可能，因此Z3可以算出有限的最优值2。

在第一个问题的约束段补充所有变量的非负断言即可得到你预期的24的结果：

(assert (>= x0 0))
(assert (>= x1 0))
(assert (>= x2 0))
(assert (>= x3 0))

添加约束后x1和x2只能取非负整数且和为1，x1最大取值为1（对应x2=0），代入计算目标值正好是24。

内容的提问来源于stack exchange，提问作者Hugues Cassé