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]))
