CP-SAT 简介：用 SAT 的技术做约束编程

CP-SAT 简介：用 SAT 的技术做约束编程#

这一章讲什么#

OR-Tools 的 CP-SAT 是 Google 开发的约束编程求解器，它与 Z3 那几章一样，都是把条件写下来让程序去找解的工具，只是它更擅长最优化，例如让利润最大、让距离最短。

这一章看四件事。

CP-SAT 的求解机制(SAT 的技术加上线性松弛)
最基本的用法(CpModel / new_int_var / add / solve)
线性规划的例题(利润最大化)
用 assumptions 推理一道逻辑谜题

四件事按顺序展开：先看机制，再看用法，最后用两道题演示。

CP-SAT 是什么#

CP-SAT 是以 SAT(可满足性问题)的技术为基础的约束编程求解器，其做法是把约束转换成 SAT 求解器能够处理的形式。它同时具备两方面的能力，一是搜索，二是优化。搜索负责在可行解之间移动，优化负责在这些解之间比较优劣。

搜索由 SAT 求解器中的那套 CDCL(遇到冲突就学习并剪枝)与 LCG(Lazy Clause Generation，惰性子句生成)技术推进
CP-SAT 还把线性松弛组合了进来，因此也能像 MIP(混合整数规划)求解器那样求目标函数的最大值或最小值

OR-Tools 里早就有 constraint_solver，那是经典的 CP 求解器，以深度优先搜索为主，最优化不是它的强项，因此现在使用 OR-Tools 时应当选 CP-SAT，这是官方推荐的用法。本书的 OrTools 章节一律使用 CP-SAT，不再涉及旧的接口。两者的接口与建模方式都不同，混用会带来额外的工作。

例题：SEND + MORE = MONEY#

用 Z3 求解 SEND+MORE=MONEY

这道字母算术在 Z3 那一章已经出现过，这里换用 CP-SAT 再解一次，基本用法的完整流程都包含在这一段代码里。同一个问题换一个求解器，写法的差异也就显现出来。

from ortools.sat.python import cp_model

model = cp_model.CpModel()
s, e, n, d, m, o, r, y = [model.new_int_var(0, 10, name) for name in "sendmory"]
model.add(s != 0)
model.add(m != 0)
model.add_all_different([s, e, n, d, m, o, r, y])
send = s * 1000 + e * 100 + n * 10 + d
more = m * 1000 + o * 100 + r * 10 + e
money = m * 10000 + o * 1000 + n * 100 + e * 10 + y

model.add(send + more == money)
solver = cp_model.CpSolver()
solver.Solve(model)
print(f"{solver.value(send)} + {solver.value(more)} = {solver.value(money)}")

9567 + 1085 = 10652

这段代码在做什么#

下面按调用顺序逐行说明，六个方法构成了 CP-SAT 的基本用法。

CpModel() … 建立一个模型，也就是装约束的容器
model.new_int_var(下限, 上限, 名字) … 声明一个整数变量
model.add(条件) … 添加约束，!=、==、>= 这类比较式原样写就行
model.add_all_different([...]) … 要求这些变量取值互不相同
solver.solve(model) … 交给求解器去求解
solver.value(式) … 取出表达式的值

六个方法之外，表达式的写法与 Python 的算术一致，只是对象换成了变量。因此照抄原来的式子通常就能用，遇到不支持的运算再改写成约束。

用 * 和 + 就能构造表达式，因此像 s * 1000 + e * 100 + ... 这样把数位照抄下来即可。要写加权和，也可以用 LinearExpr.weighted_sum()，它把每个变量的系数单独列出来。两种写法得到的表达式相同，选哪一种只取决于可读性。

send = cp_model.LinearExpr.weighted_sum([s, e, n, d], [1000, 100, 10, 1])
more = cp_model.LinearExpr.weighted_sum([m, o, r, e], [1000, 100, 10, 1])
money = cp_model.LinearExpr.weighted_sum([m, o, n, e, y], [10000, 1000, 100, 10, 1])

线性规划#

下面用一道利润最大化的题目演示线性规划，先看标准例子。

要生产产品 A 和 B，需要三种原料 a、b、c，每生产 1 单位所需的原料用量与库存列在下表中；每卖出 1 单位，A 获利 3 万日元，B 获利 2 万日元，请决定使利润最大的生产量。

原料	产品 A	产品 B	库存
a	3	1	9
b	2.5	2	12.5
c	1	2	8

设生产量分别为 \(x_1\) 和 \(x_2\)，这道题就可以写成下面这样。

目标函数

\[ z = 3x_1 + 2x_2 \quad \text{（最大化）} \]

约束条件

\[\begin{split} \begin{aligned} 3x_1 + x_2 &\leq 9 \\ 2.5x_1 + 2x_2 &\leq 12.5 \\ x_1 + 2x_2 &\leq 8 \\ x_1, x_2 &\geq 0 \end{aligned} \end{split}\]

CP-SAT 只处理整数，因此表达式中出现 2.5 时，把两边同时乘 2，把它消掉(2.5x1 + 2x2 <= 12.5 → 5x1 + 4x2 <= 25)，不等式两边同乘一个正数，条件的含义不变。系数放大之后，求出的 \(x_1, x_2\) 仍是原问题的解，不必再缩小回去。

model.maximize(z) 的含义就是去找使 \(z = 3x_1 + 2x_2\) 取最大值的 \(x_1, x_2\)。minimize() 与之对称，改成求最小值即可。

model = cp_model.CpModel()
x1, x2 = [model.new_int_var(0, 10000, f"x{i}") for i in range(1, 3)]
model.add(3 * x1 + x2 <= 9)
model.add(5 * x1 + 4 * x2 <= 25)
model.add(x1 + 2 * x2 <= 8)
z = 3 * x1 + 2 * x2
model.maximize(z)
solver = cp_model.CpSolver()
solver.Solve(model)
print(f"x1 = {solver.value(x1)}, x2 = {solver.value(x2)}, z = {solver.value(z)}")

x1 = 2, x2 = 3, z = 12

逻辑谜题#

有红、蓝、黄、绿四个箱子，其中若干个箱子里放着苹果(至少有一个，两个、三个也可以)。规则是可以从这些箱子中挑一个，把里面的苹果拿走。

请根据下面的两条线索，选出一定装着苹果的那只箱子。

红箱子里有苹果的话，蓝箱子里也有苹果
绿箱子里没有苹果的话，黄箱子和蓝箱子里都没有苹果

在 CP-SAT 中，用布尔变量加逻辑约束就能把这两句话原样写下来，剩下的推理交给求解器。线索只有两条，组合起来却足以定位到具体的那一只箱子。变量只有四个，穷举也能做完，这里要看的是把条件写成约束的方式。

model = cp_model.CpModel()
red, blue, yellow, green = [model.new_bool_var(name) for name in ['red', 'blue', 'yellow', 'green']]

model.add_bool_or([red, blue, yellow, green])                 # 至少有 1 个
model.add_implication(red, blue)                               # 红 → 蓝
model.add_bool_and(~yellow, ~blue).only_enforce_if(~green)     # 没有绿 → 黄和蓝也没有

solver = cp_model.CpSolver()
for box in [red, blue, yellow, green]:
    model.add_assumption(~box)          # 假设“这个箱子里没有”
    res = solver.solve(model)
    if res == cp_model.INFEASIBLE:      # 矛盾 → 一定放着
        print(box)
    model.clear_assumptions()           # 删掉假设

green

这几行代码在做什么#

new_bool_var() … 建立一个 0/1 的布尔变量
add_bool_or([...]) … 至少有一个为真(逻辑或)
add_implication(a, b) … a 成立就要求 b(逻辑蕴含)
add_bool_and(a, b).only_enforce_if(c) … 只在 c 成立时要求“a 且 b”
- ~ 表示取反
- only_enforce_if() 指定“只在这个条件成立时才有效”

这道谜题要的不是随便找到一个解，而是推理出哪个箱子一定装着苹果。因此对每个箱子，先假设“里面没有”再去求解，如果出现矛盾(INFEASIBLE)，就说明这个箱子里一定有苹果。

用 model.add_assumption(条件) 添加假设
用 clear_assumptions() 清除假设(试下一个箱子之前必须调用)

假设会留在模型里；如果漏掉清除，下一个箱子就会带上上一个箱子的条件。

结果落在 green 上。其中的道理是：如果没有绿箱，黄箱和蓝箱也就都没有；再由红→蓝这条线索，红箱也不能有，结果一个苹果都不剩。逐个假设、逐个排除，这个过程与手算一致，只是由求解器完成。

小结#

CP-SAT 靠两部分工作：SAT 技术与线性松弛，用 OR-Tools 就选它
基本流程是 CpModel() → 变量 → add() → solve() → value()
要做最优化，用 model.maximize(式) / model.minimize(式)
CP-SAT 只处理整数；表达式里有小数时，两边同乘一个整数把它消掉
用布尔变量配逻辑约束(add_bool_or、add_implication、only_enforce_if)，条件分支也写得出来
用 assumptions 可以询问“再加上这个条件会不会矛盾”，推理谜题就靠它

下一章将详细介绍 CP-SAT 各种 API 函数的用法。