cp-sat求解器介绍及使用案例-阿里云开发者社区

ortools是Google开发的一套优化工具，其中ortools中自带的cp-sat是一个用于求解约束规划问题的求解器。本文介绍一下cp-sat的求解原理和基础应用。

cp-sat求解器介绍

cp-sat的原理是基于有限域上的布尔可满足性问题（SAT）和伪布尔优化（PBO）。它将约束规划问题转化为一个整数线性规划（ILP）问题，并使用启发式搜索和冲突分析等技术来寻找最优解或证明无解。

它可以处理整数变量、布尔变量、线性约束、全局约束、指示器约束等。
它可以处理多目标优化问题，并支持词典序或分层方法。
它可以利用多核处理器并行计算，并提供超时和中断功能。
它可以输出详细的求解过程信息，包括冲突数、支配数、重启数等。

cp-sat的求解过程

预处理

将约束规划问题转化为一个整数线性规划（ILP）问题，并进行一些简化和优化，如删除冗余变量和约束、合并等价变量和约束、检测对称性和支配性等。

搜索

使用启发式搜索策略在可行解空间中寻找最优解或证明无解。搜索过程中会使用冲突分析、重启、剪枝等技术来加速求解过程。

输出

输出最优解或无解的结果，并给出一些求解过程的信息，如冲突数、支配数、重启数等。

cp-sat的搜索策略

cp-sat的搜索策略是基于有限域上的布尔可满足性问题（SAT）和伪布尔优化（PBO）。它将整数变量和布尔变量都编码为二进制位向量，并使用布尔逻辑运算来表示约束条件。它使用了一种叫做CDCL（conflict-driven clause learning）的算法来进行搜索。

CDCL算法步骤

选择一个未赋值的变量，并给它一个随机或启发式的值，这叫做猜测（guess）。
根据已赋值的变量和约束条件，推导出其他变量的值，这叫做传播（propagate）。
如果没有发生冲突，即所有约束都被满足，那么继续选择下一个未赋值的变量并重复上述步骤；如果发生了冲突，即有某个约束被违反了，那么回溯到上一个猜测点，并改变该猜测点的值，这叫做回溯（backtrack）。
在回溯过程中，还会根据冲突原因学习出新的约束条件，并加入到原始问题中，这叫做学习（learn）。学习出来的新约束可以帮助剪枝去掉一些不可行或次优的分支，从而缩小搜索空间。

cp-sat使用技术

使用多线程并行计算，同时进行多个搜索过程，并共享学习出来的新约束。
使用分层方法来处理多目标优化问题，即按照目标函数的优先级依次求解，每次求解时将上一个目标函数的最优值作为约束条件。
使用词典序方法来处理多目标优化问题，即将多个目标函数组合成一个单一的目标函数，按照词典序比较不同解的优劣。
使用线性化技术来处理非线性约束，即将非线性约束转化为一系列的线性约束和变量。

cp-sat可解决的问题

cp-sat可以用来解决各种约束规划问题，如排程、布局、分配、选址等。以下是一些常见的案例：

排程问题：给定一组任务和一组资源，如工人、机器、车辆等，每个任务有一定的持续时间和优先级，每个资源有一定的可用时间和容量，求解如何安排任务到资源上，使得满足所有约束条件，并最大化或最小化某个目标函数，如完成时间、成本、利润等。
装载问题：给定一组物品和一个容器，如箱子、背包、棋盘等，每个物品有一定的形状和大小，每个容器有一定的尺寸和限制，求解如何放置物品到容器中，使得满足所有约束条件，并最大化或最小化某个目标函数，如占用空间、重量、价值等。
分配问题：给定一组代表人或物的节点和一组代表关系或需求的边，每个节点有一定的属性和限制，每条边有一定的权重和方向，求解如何分配节点到不同的集合或角色中，使得满足所有约束条件，并最大化或最小化某个目标函数，如总权重、平衡度、公平度等。
选址问题：给定一个地图上的一组候选位置和一组需求点，每个候选位置有一定的成本和收益，每个需求点有一定的数量和距离限制，求解如何选择若干候选位置作为服务点或设施点，并分配需求点到服务点或设施点上，使得满足所有约束条件，并最大化或最小化某个目标函数，如总收益、总成本、总距离等。

cp-sat案例

案例1：简单线性规划问题

有两种产品A和B，每种产品需要不同数量的原料X和Y。每单位A需要3单位X和2单位Y，每单位B需要4单位X和3单位Y。每天最多可以生产1000单位X和800单位Y。每单位A的利润是25元，每单位B的利润是30元。问如何安排生产计划，使得总利润最大？

from ortools.sat.python import cp_model
# 创建模型
model = cp_model.CpModel()
# 定义变量
x = model.NewIntVar(0, 1000, 'x') # 生产A的数量
y = model.NewIntVar(0, 1000, 'y') # 生产B的数量
# 定义目标函数
profit = model.NewIntVar(0, 1000000, 'profit') # 总利润
model.Add(profit == 25 * x + 30 * y) # 利润等于单价乘以数量
model.Maximize(profit) # 最大化利润
# 定义约束条件
model.Add(3 * x + 4 * y <= 1000) # 原料X的限制
model.Add(2 * x + 3 * y <= 800) # 原料Y的限制
# 创建求解器并求解模型
solver = cp_model.CpSolver()
status = solver.Solve(model)
# 打印结果
if status == cp_model.OPTIMAL:
    print('最优解：')
    print('生产A：', solver.Value(x))
    print('生产B：', solver.Value(y))
    print('总利润：', solver.Value(profit))
else:
    print('没有找到最优解')

案例2：分配问题

这个案例是使用CP-SAT求解器来解决一个分配问题。分配问题是指将一组任务分配给一组工人，使得每个任务只能由一个工人完成，每个工人只能完成一个任务，且总成本最小。

from ortools.sat.python import cp_model
# 创建模型
model = cp_model.CpModel()
# 定义数据
num_workers = 4 # 工人数量
num_tasks = 4 # 任务数量
costs = [ # 每个工人完成每个任务的成本矩阵
    [90, 76, 75, 70],
    [35, 85, 55, 65],
    [125, 95, 90, 105],
    [45, 110, 95, 115],
]
# 定义变量
x = [] # x[i][j]表示第i个工人是否被分配到第j个任务，取值为0或1
for i in range(num_workers):
    t = []
    for j in range(num_tasks):
        t.append(model.NewBoolVar('x[%i,%i]' % (i,j)))
    x.append(t)
# 定义约束条件
# 每个工人只能被分配到一个任务
for i in range(num_workers):
    model.Add(sum(x[i][j] for j in range(num_tasks)) == 1)
# 每个任务只能被分配给一个工人
for j in range(num_tasks):
    model.Add(sum(x[i][j] for i in range(num_workers)) == 1)
# 定义目标函数：最小化总成本
objective_terms = []
for i in range(num_workers):
    for j in range(num_tasks):
        objective_terms.append(costs[i][j] * x[i][j])
model.Minimize(sum(objective_terms))
# 创建求解器并求解模型
solver = cp_model.CpSolver()
status = solver.Solve(model)
if status == cp_model.OPTIMAL:
    print('Total cost: %i' % solver.ObjectiveValue())
    print()
    for i in range(num_workers):
        for j in range(num_tasks):
            if solver.Value(x[i][j]) == True:
                print('Worker %i assigned to task %i. Cost: %i' %
                      (i,j,costs[i][j]))

cp-sat求解器介绍及使用案例