最大化网格第13大元素：Z3Py整数规划技术问询

问题描述 #

• 拥有48×3的IntVectors类型numpy数组X（数组各分段存在约束），以及48×1的预定义整数常量数组initial_scores。
• 需要在给定约束下，最大化行和的第13大值：行和计算式为[initial_scores[k] + X[k, 0] + X[k, 1] + X[k, 2] for k in range(48)]，将所有行和降序排序后取第13个元素。
• 尝试使用文献提到的nth和mk_seq_nth函数，但发现二者未定义，怀疑使用方式错误或Z3Py不支持该函数。

解决方案：手动建模第13大值约束 #

Z3Py并未内置直接获取排序后第n个元素的nth或mk_seq_nth函数，可通过引入目标变量并添加约束的方式实现需求：

1. 定义target变量表示要最大化的第13大行和。
2. 添加约束：至少有13个行和大于等于target（保证target不低于第13大值）。
3. 添加约束：至少有36个行和小于等于target（保证target不高于第13大值）。

代码示例 #

import z3
import numpy as np

# 预定义initial_scores（示例数据，替换为实际值）
initial_scores = np.random.randint(0, 100, size=(48,))
# 创建48×3的IntVector数组X
X = np.array([[z3.Int(f"X_{k}_{col}") for col in range(3)] for k in range(48)])

# 初始化优化求解器
opt = z3.Optimize()

# 添加X的分段约束（示例约束，替换为实际业务约束）
# 前16行：行和≤10
for k in range(16):
    opt.add(X[k,0] + X[k,1] + X[k,2] <= 10)
# 中间16行：行和≥5
for k in range(16, 32):
    opt.add(X[k,0] + X[k,1] + X[k,2] >= 5)
# 后16行：每个元素在0-20之间
for k in range(32, 48):
    for col in range(3):
        opt.add(X[k, col] >= 0)
        opt.add(X[k, col] <= 20)

# 计算所有行和
row_sums = [initial_scores[k] + X[k,0] + X[k,1] + X[k,2] for k in range(48)]

# 定义目标变量：第13大的行和
target = z3.Int("target")

# 约束1：至少13个行和≥target
count_ge = z3.Sum([z3.If(rs >= target, 1, 0) for rs in row_sums])
opt.add(count_ge >= 13)

# 约束2：至少36个行和≤target（即最多12个行和>target）
count_le = z3.Sum([z3.If(rs <= target, 1, 0) for rs in row_sums])
opt.add(count_le >= 36)

# 最大化目标变量
max_target = opt.maximize(target)

# 求解并输出结果
if opt.check() == z3.sat:
    print(f"最大的第13大行和为: {opt.model()[target]}")
    # 若需验证X的值，可取消以下注释
    # for k in range(48):
    #     x_vals = [opt.model()[X[k, col]].as_long() for col in range(3)]
    #     print(f"X[{k}]: {x_vals}, 行和: {initial_scores[k] + sum(x_vals)}")
else:
    print("问题无解")

说明 #

Z3Py标准API中不存在nth或mk_seq_nth函数，这类函数可能是特定文献或自定义工具中的实现。通过上述约束建模的方式，无需依赖非标准函数即可实现最大化第13大行和的需求。

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