OR-Tools CP-SAT求解器：如何约束约2/3的IntVar值小于400？

核心方案还是用BoolVar，之前尝试失败大概率是没做好双向约束或者总和范围设置，具体步骤如下：

• 为字典里的每个日期IntVar配对一个BoolVar，用1标记变量<400，0标记>=400
• 给每对变量添加双向约束：
  • 当BoolVar=1时，强制对应的日期变量小于400
  • 当BoolVar=0时，强制对应的日期变量大于等于400
• 统计总变量数，约束所有BoolVar的总和落在2/3总数量的附近区间（比如至少达到2/3，或者设上下限让结果更接近）

代码示例 #

from ortools.sat.python import cp_model

model = cp_model.CpModel()

# 假设你的日期变量字典是date_vars，键为任务标识，值为IntVar类型的日期变量
date_vars = {
    "task_01": model.NewIntVar(0, 500, "task_01_date"),
    "task_02": model.NewIntVar(0, 500, "task_02_date"),
    "task_03": model.NewIntVar(0, 500, "task_03_date"),
    "task_04": model.NewIntVar(0, 500, "task_04_date"),
    "task_05": model.NewIntVar(0, 500, "task_05_date"),
    "task_06": model.NewIntVar(0, 500, "task_06_date"),
    # 可继续添加更多变量
}

# 1. 创建对应BoolVar字典，标记每个日期变量是否小于400
lt_400_flags = {}
for task_id, date_var in date_vars.items():
    lt_400_flags[task_id] = model.NewBoolVar(f"{task_id}_lt_400")

# 2. 添加双向约束，绑定BoolVar和日期变量的取值关系
for task_id, date_var in date_vars.items():
    flag = lt_400_flags[task_id]
    # 当flag为1时，日期变量必须<400
    model.Add(date_var < 400).OnlyEnforceIf(flag)
    # 当flag为0时，日期变量必须>=400
    model.Add(date_var >= 400).OnlyEnforceIf(flag.Not())

# 3. 约束BoolVar总和满足约2/3的要求
total_count = len(date_vars)
# 计算最小需要满足的数量，用四舍五入确保接近2/3
min_required = round(total_count * 2 / 3)
# 如果需要更严格的“约”，可以同时设置上下限，比如允许±1的误差
max_required = total_count - (total_count // 3)
model.Add(min_required <= sum(lt_400_flags.values()) <= max_required)

# 求解并输出结果
solver = cp_model.CpSolver()
status = solver.Solve(model)

if status in [cp_model.OPTIMAL, cp_model.FEASIBLE]:
    print("求解成功，结果如下：")
    for task_id, date_var in date_vars.items():
        print(f"{task_id}: 日期={solver.Value(date_var)}, 是否<400={bool(solver.Value(lt_400_flags[task_id]))}")
else:
    print("无解")

关键注意点 #

• 必须添加双向约束，否则BoolVar和日期变量的取值会脱节，导致约束不生效
• 总和约束的范围可以根据需求调整：如果只要求“至少2/3”，就只加下限；如果要严格接近2/3，就同时设置上下限，避免出现所有变量都<400的情况

内容的提问来源于stack exchange，提问作者andré amistadi