如何使用CP-SAT类方法实现多约束逻辑或？求示例代码

当然可以用CP-SAT实现(x + y >=10) ∨ (x - y <= 5) ∨ (y >= 2)这类逻辑或约束，布尔变量是关键工具，结合你熟悉的大M法就能轻松转化为CP-SAT可处理的形式。

核心思路 #

给每个子约束分配一个布尔变量：

• b1为真时，x + y >=10必须成立；
• b2为真时，x - y <=5必须成立；
• b3为真时，y >=2必须成立；

然后通过AddBoolOr要求至少一个布尔变量为真，再用大M法（配合CP-SAT的OnlyEnforceIf方法）把布尔变量和对应子约束绑定，确保布尔变量的真假状态和子约束的成立状态一致。

示例代码（Python + OR-Tools CP-SAT） #

from ortools.sat.python import cp_model

def main():
    # 初始化CP-SAT模型
    model = cp_model.CpModel()

    # 定义整数变量x和y，可根据实际需求调整取值范围
    x = model.NewIntVar(0, 20, 'x')
    y = model.NewIntVar(0, 20, 'y')

    # 为每个子约束创建对应的布尔变量
    b1 = model.NewBoolVar('b1')  # 对应 x + y >= 10
    b2 = model.NewBoolVar('b2')  # 对应 x - y <= 5
    b3 = model.NewBoolVar('b3')  # 对应 y >= 2

    # 用大M法绑定布尔变量与子约束
    # 选择M时，只要覆盖变量可能的极值范围即可，这里x,y最大20，M=40足够
    M = 40

    # 处理b1：b1为真时强制执行x+y>=10，为假时强制执行x+y<=9（即不满足x+y>=10）
    model.Add(x + y >= 10).OnlyEnforceIf(b1)
    model.Add(x + y <= 9).OnlyEnforceIf(cp_model.Not(b1))

    # 处理b2：b2为真时强制执行x-y<=5，为假时强制执行x-y>=6
    model.Add(x - y <= 5).OnlyEnforceIf(b2)
    model.Add(x - y >= 6).OnlyEnforceIf(cp_model.Not(b2))

    # 处理b3：b3为真时强制执行y>=2，为假时强制执行y<=1
    model.Add(y >= 2).OnlyEnforceIf(b3)
    model.Add(y <= 1).OnlyEnforceIf(cp_model.Not(b3))

    # 核心逻辑或约束：至少一个布尔变量为真，即至少一个子约束成立
    model.AddBoolOr([b1, b2, b3])

    # 创建求解器并求解
    solver = cp_model.CpSolver()
    status = solver.Solve(model)

    # 输出求解结果
    if status in (cp_model.OPTIMAL, cp_model.FEASIBLE):
        print(f"x = {solver.Value(x)}")
        print(f"y = {solver.Value(y)}")
        print(f"b1（x+y>=10）是否成立: {solver.BooleanValue(b1)}")
        print(f"b2（x-y<=5）是否成立: {solver.BooleanValue(b2)}")
        print(f"b3（y>=2）是否成立: {solver.BooleanValue(b3)}")
    else:
        print("该约束下没有可行解")

if __name__ == '__main__':
    main()

关键细节说明 #

• OnlyEnforceIf(b)是CP-SAT中控制约束生效时机的核心方法，只有当布尔变量b为真时，对应的约束才会被激活。
• 大M的取值不需要精确，只要足够大到不会限制变量的合理取值即可，避免因M过小导致约束冲突。
• AddBoolOr直接实现了多个布尔变量的逻辑或关系，完美对应原问题的∨需求。

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