Z3优化器求解整数约束下变量最大值返回非最优结果问题咨询

• 你使用的Z3 4.8.7为较老版本，该版本的整数线性优化模块存在已知缺陷，多变量线性目标最大化场景下会错误返回局部最优解而非全局最优解。
• 你的测试代码注释了(set-logic QF_LIA)声明，Z3无法提前识别当前为无量词整数线性逻辑场景，会调用通用启发式优化策略，不会启用适配QF_LIA的精准求解器。

SMT-LIB 侧修复 #

方案1：升级Z3版本（推荐） #

升级Z3到4.12及以上稳定版本，该缺陷已经被官方修复，仅需取消(set-logic QF_LIA)的注释即可得到正确结果，修复后代码示例：

(set-logic QF_LIA)
(define-const x Int 9)

(define-const a Int 3)
(define-const b Int 4)
(define-const c Int 4)
(define-const d Int 5)

(declare-const i Int)
(declare-const j Int)
(declare-const t Int)
(declare-const r Int)

(assert (>= i 0))
(assert (>= j 0))

(assert (= t (+ (* i b) (* j d) 1)))
(assert (= r (+ (* i a) (* j c) c)))

(assert (<= t x))

(maximize r)
(check-sat)
(get-value (r))

运行后会直接返回((r 10))的正确结果。

方案2：兼容旧版本配置 #

如果必须保留Z3 4.8.7版本，可添加(set-option :opt.priority box)配置项，强制优化器采用边界扫描模式求解全局最优，修改后代码示例：

(set-logic QF_LIA)
(set-option :opt.priority box)
(define-const x Int 9)

(define-const a Int 3)
(define-const b Int 4)
(define-const c Int 4)
(define-const d Int 5)

(declare-const i Int)
(declare-const j Int)
(declare-const t Int)
(declare-const r Int)

(assert (>= i 0))
(assert (>= j 0))

(assert (= t (+ (* i b) (* j d) 1)))
(assert (= r (+ (* i a) (* j c) c)))

(assert (<= t x))

(maximize r)
(check-sat)
(get-value (r))

Python 调用侧修复 #

首先升级z3-solver依赖到最新版本：

pip install --upgrade z3-solver

修复后的调用代码示例如下，无需手动迭代添加约束：

import z3

opt = z3.Optimize()
# 若需兼容旧版本Z3，可添加以下配置行
# opt.set(priority='box')

# 变量定义
i = z3.Int('i')
j = z3.Int('j')
t = z3.Int('t')
r = z3.Int('r')

# 常量定义
x = 9
a, b, c, d = 3, 4, 4, 5

# 添加约束
opt.add(i >= 0, j >= 0)
opt.add(t == i * b + j * d + 1)
opt.add(r == i * a + j * c + c)
opt.add(t <= x)

# 最大化目标
opt.maximize(r)

# 求解输出
print(opt.check())
print(opt.model()[r])

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