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

cp-sat求解器介绍

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

cp-sat的求解过程

预处理

搜索

输出

cp-sat的搜索策略

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

CDCL算法步骤

• 选择一个未赋值的变量，并给它一个随机或启发式的值，这叫做猜测（guess）。

• 根据已赋值的变量和约束条件，推导出其他变量的值，这叫做传播（propagate）。

• 如果没有发生冲突，即所有约束都被满足，那么继续选择下一个未赋值的变量并重复上述步骤；如果发生了冲突，即有某个约束被违反了，那么回溯到上一个猜测点，并改变该猜测点的值，这叫做回溯（backtrack）。

• 在回溯过程中，还会根据冲突原因学习出新的约束条件，并加入到原始问题中，这叫做学习（learn）。学习出来的新约束可以帮助剪枝去掉一些不可行或次优的分支，从而缩小搜索空间。

cp-sat使用技术

• 使用多线程并行计算，同时进行多个搜索过程，并共享学习出来的新约束。

• 使用分层方法来处理多目标优化问题，即按照目标函数的优先级依次求解，每次求解时将上一个目标函数的最优值作为约束条件。

• 使用词典序方法来处理多目标优化问题，即将多个目标函数组合成一个单一的目标函数，按照词典序比较不同解的优劣。

• 使用线性化技术来处理非线性约束，即将非线性约束转化为一系列的线性约束和变量。

cp-sat可解决的问题

• 排程问题：给定一组任务和一组资源，如工人、机器、车辆等，每个任务有一定的持续时间和优先级，每个资源有一定的可用时间和容量，求解如何安排任务到资源上，使得满足所有约束条件，并最大化或最小化某个目标函数，如完成时间、成本、利润等。

• 装载问题：给定一组物品和一个容器，如箱子、背包、棋盘等，每个物品有一定的形状和大小，每个容器有一定的尺寸和限制，求解如何放置物品到容器中，使得满足所有约束条件，并最大化或最小化某个目标函数，如占用空间、重量、价值等。

• 分配问题：给定一组代表人或物的节点和一组代表关系或需求的边，每个节点有一定的属性和限制，每条边有一定的权重和方向，求解如何分配节点到不同的集合或角色中，使得满足所有约束条件，并最大化或最小化某个目标函数，如总权重、平衡度、公平度等。

• 选址问题：给定一个地图上的一组候选位置和一组需求点，每个候选位置有一定的成本和收益，每个需求点有一定的数量和距离限制，求解如何选择若干候选位置作为服务点或设施点，并分配需求点到服务点或设施点上，使得满足所有约束条件，并最大化或最小化某个目标函数，如总收益、总成本、总距离等。

cp-sat案例

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

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：分配问题

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