Z3优化器：寻找输入变量最少修改次数的最优赋值方案

需求：给变量x1、x2、x3找到不同的合法赋值，要求最小化对初始值（x1=0、x2=1、x3=1）的修改次数，约束条件为 y = x1 + x2 - x3 且 y = 0。

原代码问题说明 #

原代码存在几处语法和用法错误：

• 未将x1、x2、x3、y声明为Z3的整数变量，直接用普通Python变量无法被Z3识别
• 约束中判断相等误用了赋值符号=，Z3里需用==
• Goal对象的用法不符合当前场景，直接用优化求解器Optimize即可

修正后的实现代码 #

要实现最小化修改次数的需求，需使用Z3的Optimize求解器，定义修改次数目标并最小化：

from z3 import *

# 声明Z3整数变量
x1, x2, x3, y = Ints('x1 x2 x3 y')
# 记录初始值
init_x1, init_x2, init_x3 = 0, 1, 1

# 创建优化求解器实例
opt = Optimize()

# 添加核心约束条件
opt.add(y == x1 + x2 - x3)
opt.add(y == 0)

# 计算修改次数：变量与初始值不同则计1次，求和得到总修改次数
changes = If(x1 != init_x1, 1, 0) + If(x2 != init_x2, 1, 0) + If(x3 != init_x3, 1, 0)

# 设置优化目标：最小化修改次数
opt.minimize(changes)

# 求解并输出所有满足最小修改次数的不同赋值
print("最小修改次数的所有解：")
while opt.check() == sat:
    model = opt.model()
    x1_val = model[x1].as_long()
    x2_val = model[x2].as_long()
    x3_val = model[x3].as_long()
    print(f"x1={x1_val}, x2={x2_val}, x3={x3_val}，修改次数：{model.eval(changes).as_long()}")
    # 添加约束排除当前解，继续寻找下一个不同赋值
    opt.add(Or(x1 != x1_val, x2 != x2_val, x3 != x3_val))

代码说明 #

• 选用Optimize而非普通Solver，因为需要完成「最小化修改次数」的优化目标
• 通过If表达式逐个判断变量是否修改，求和得到总修改次数作为优化对象
• 循环求解并输出所有符合要求的不同赋值，每次求解后添加约束排除当前解，避免重复输出

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