↓

排课问题不是玄学：SAT、0-1规划与 CP-SAT 的建模思路

··
技术思考 运筹优化 SAT CP-SAT 排课 组合优化

每到开学前，排课都是一件让人头疼的事。

表面上看，排课只是把课程填进时间表；但真正做起来会发现，它牵涉到班级、老师、课程、教室、时间等多个因素。一个老师不能同时教两个班，一个班不能同时上两门课，教室不能重复占用，数学课最好排上午，体育课别排太晚……

所以，排课并不是"凭经验填表"，它本质上是一个典型的组合优化问题。

一、把排课问题数学化 #

数学建模的第一步，是把生活语言翻译成数学语言。

排课问题通常可以拆成三部分：

模块含义
变量哪些事情需要决定
约束哪些安排不允许
目标什么样的课表更好

例如，我们需要决定：

某个班级，在某个时间，由某个老师，在某个教室，上某门课。

于是可以定义一个 0-1 变量：

$$ x_{c,s,t,p,r} \in \{0,1\} $$

其中：

  • \(c\)：班级
  • \(s\)：课程
  • \(t\)：教师
  • \(p\)：时间槽
  • \(r\)：教室

含义是：

$$ x_{c,s,t,p,r}=1 $$

表示"班级 \(c\) 在时间 \(p\)，教室 \(r\)，由老师 \(t\) 上课程 \(s\)"；否则为 0。

这就是排课问题数字化的核心：

一张课表，本质上就是大量 0 和 1 的组合。

不过需要注意，五维变量的规模会迅速膨胀——以一个中等规模学校为例：30个班 × 15门课 × 50位教师 × 35个时间槽 × 40间教室，变量数可达数十亿级别。因此在实际建模中，通常会根据问题结构进行降维，我们稍后会看到。

二、用 0-1 规划表达排课约束 #

有了变量，就可以写约束。

1. 一个班同一时间最多上一门课 #

对固定班级 \(c\) 和时间 \(p\)，所有课程、教师、教室的安排加起来不能超过 1：

$$ \sum_{s,t,r} x_{c,s,t,p,r} \le 1 $$

这表示：

一个班不能在同一节课同时上数学和英语。

2. 一个老师同一时间最多上一节课 #

对固定教师 \(t\) 和时间 \(p\)：

$$ \sum_{c,s,r} x_{c,s,t,p,r} \le 1 $$

这表示：

张老师不能在周一第 1 节同时教 1 班和 2 班。

3. 一个教室同一时间最多被一个班使用 #

对固定教室 \(r\) 和时间 \(p\)：

$$ \sum_{c,s,t} x_{c,s,t,p,r} \le 1 $$

这表示：

同一个教室不能在同一时间被多个班占用。

4. 每门课的周课时必须满足 #

如果班级 \(c\) 的课程 \(s\) 每周需要 \(h_{c,s}\) 节，那么：

$$ \sum_{t,p,r} x_{c,s,t,p,r} = h_{c,s} $$

比如：

初一 1 班数学每周 5 节，就必须刚好排 5 节。

三、SAT：把排课看成真假判断 #

SAT 问题，全称是布尔可满足性问题（Boolean Satisfiability Problem）。它问的是：

是否存在一组 True / False 赋值，使所有逻辑条件都成立？

在排课中，每一个可能安排都可以看成一个布尔变量：

$$ A = \text{"张老师周一第1节教1班数学"} $$

如果安排发生，\(A=True\)；否则 \(A=False\)。

如果两个安排不能同时发生，比如：

  • \(A\)：张老师周一第 1 节教 1 班
  • \(B\)：张老师周一第 1 节教 2 班

那么可以写成逻辑子句：

$$ \neg A \lor \neg B $$

意思是：

A 和 B 不能同时为真。

如果某门课必须在若干候选时间中选一个，可以写成：

$$ A_1 \lor A_2 \lor A_3 \lor \cdots \lor A_n $$

意思是：

至少有一个安排必须发生。

所以，SAT 适合回答一个问题：

是否存在一张满足所有硬约束的课表？

值得注意的是，SAT 问题的表达能力等价于 0-1 规划——每一个 0-1 线性约束都可以通过辅助变量转化为 CNF 子句，反之亦然。两者的区别不在于"能不能表达"，而在于求解策略：SAT 求解器擅长布尔推理和冲突学习，0-1 规划求解器擅长线性松弛和割平面。CP-SAT 则融合了两者。

四、CDCL：SAT 求解器为什么快？ #

现代 SAT 求解器通常使用 CDCL 算法。

CDCL 是：

Conflict-Driven Clause Learning 冲突驱动子句学习

它的思路很像人排课：

  1. 先尝试安排一部分课程
  2. 发现某些安排导致冲突
  3. 分析冲突原因
  4. 记录一条新规则
  5. 以后避免重复犯错

例如，求解器尝试：

张老师周一第 1 节教 1 班数学

后面发现这样会导致其他班的数学课无法安排。普通搜索可能只是回退重试，而 CDCL 会学习到：

某些组合不能同时出现。

这样下一次搜索时，它就不会再走同样的死路。

这就是现代 SAT 求解器强大的原因：

它不是盲目枚举，而是在失败中学习。

CDCL 的核心机制包括：

  • 冲突分析（Conflict Analysis）：当赋值导致子句为假时，回溯分析哪些决策引发了冲突
  • 子句学习（Clause Learning）：将冲突原因编码为新子句，永久加入子句库
  • 非时间序回跳（Non-chronological Backjumping）：不必逐层回退，可以直接跳过无关的决策层
  • 重启策略（Restart Strategy）：定期重置搜索状态，避免陷入局部搜索陷阱

这些技术使得 CDCL 能够处理包含数百万变量的工业级 SAT 实例。

五、从 0-1 规划到 CP-SAT #

0-1 规划已经可以很好地描述排课问题：

$$ x_i \in \{0,1\} $$

再配合各种线性约束，就可以构造一个完整模型。

但真实排课往往不只有硬约束，还有大量偏好：

  • 数学尽量排上午
  • 体育不要排最后一节
  • 老师尽量不要一天排太满
  • 同一门课尽量分散
  • 教师空档尽量少
  • 班级教室尽量固定

这些规则如果全部用传统 0-1 规划表达，往往需要很多辅助变量，模型会变得复杂。

这时，CP-SAT 更适合。

CP-SAT 可以理解为：

约束规划 + SAT 冲突学习 + 整数优化

它既能处理 0-1 变量和线性约束，也能处理逻辑条件、软约束和优化目标。

例如，对于软约束，我们可以设计惩罚变量：

$$ penalty_i \in \{0,1\} $$

如果违反某个偏好，就让 \(penalty_i=1\)。最终目标是：

$$ \min \sum_i w_i \cdot penalty_i $$

其中 \(w_i\) 是惩罚权重。

也就是说：

先保证课表合法，再让课表尽量好看。

CP-SAT 的求解过程融合了多种技术：预处理阶段的约束传播和变量固定，搜索阶段的 SAT 引擎与线性松弛交替推进，以及定期的 Large Neighborhood Search 来跳出局部最优。这种"混合引擎"架构使它在排课等实际问题上的表现远超单一策略的求解器。

六、硬约束与软约束 #

排课模型中，约束通常分成两类。

硬约束：必须满足 #

这些规则一旦违反，课表就是非法的：

  • 一个班同一时间只能上一门课
  • 一个老师同一时间只能上一节课
  • 一个教室同一时间只能被一个班使用
  • 每门课的周课时必须满足
  • 老师不能在不可用时间上课

硬约束决定：

课表能不能用。

软约束：尽量满足 #

这些规则不一定绝对禁止，但越满足越好：

  • 主课尽量上午
  • 体育尽量不要太晚
  • 老师空档尽量少
  • 同一课程不要集中在一天
  • 老师一天不要连续上太多节

软约束决定：

课表好不好用。

在 CP-SAT 中，通常会把软约束转化为惩罚项，然后最小化总惩罚：

$$ \min \left( w_1p_1 + w_2p_2 + \cdots + w_np_n \right) $$

软约束的权重设计是一个需要经验的过程。权重过低，求解器可能轻易违反；权重过高，又可能挤压其他偏好的满足空间。实际操作中，可以先用统一权重求解，再根据结果微调——哪些偏好几乎总是被违反，就适当提高它的权重。

七、一个简化版建模思路 #

如果先不考虑教室（大多数中学的班级教室是固定的），可以把变量简化成：

$$ x_{c,s,p} \in \{0,1\} $$

表示：

班级 \(c\) 在时间 \(p\) 是否上课程 \(s\)。

这个降维效果显著：30个班 × 15门课 × 35个时间槽 = 15,750 个变量，相比五维的数十亿，已经可以轻松求解了。

基本约束包括：

每个班每个时间最多一门课 #

$$ \sum_s x_{c,s,p} \le 1 $$

每门课课时满足要求 #

$$ \sum_p x_{c,s,p} = h_{c,s} $$

教师不能冲突 #

如果教师 \(t\) 负责若干班级课程组合 \((c,s)\)，那么：

$$ \sum_{(c,s)\in T_t} x_{c,s,p} \le 1 $$

其中 \(T_t\) 表示教师 \(t\) 负责的课程集合。

不可用时间禁止排课 #

如果某老师或班级在时间 \(p\) 不可用，则：

$$ x_{c,s,p}=0 $$

这个模型虽然简化，但已经包含排课系统的核心骨架。在这个基础上，可以逐步加入软约束（如课程分散、主课优先上午等），构建一个完整的优化模型。

八、编程实现建议 #

如果想真正动手做一个排课程序，推荐从：

1

Python + OR-Tools CP-SAT

开始。

原因很简单：

  • Python 适合快速建模
  • OR-Tools 提供成熟的 CP-SAT 求解器
  • 可以同时处理硬约束和软约束
  • 能设置求解时间，比如 30 秒内给出一个较好方案
  • 非常适合教学、比赛建模和原型开发

如果你更熟悉 Go，也可以用 Go 做系统后端，把求解模块交给 Python 微服务，通过 HTTP/gRPC 交互——求解本身并不高频，架构上完全解耦。直接在 Go 中绑定 OR-Tools 也有社区方案，但跨语言维护成本较高，不推荐作为首选。

一个典型的最小实现流程：

  1. 定义数据结构：班级、教师、课程、时间槽、课时需求
  2. 创建 CP-SAT 模型，声明布尔变量 \(x_{c,s,p}\)
  3. 逐一添加硬约束
  4. 将软约束转化为惩罚项，设定目标函数
  5. 调用求解器，设置时间限制
  6. 从解中提取课表，格式化输出

九、总结 #

排课问题不是玄学。

它可以被清晰地建模为：

  • SAT 问题：判断是否存在合法课表
  • 0-1 规划问题：用二进制变量和线性约束描述安排
  • CP-SAT 问题：同时处理硬约束、软约束与优化目标

从 SAT 的可满足性判断，到 0-1 规划的约束表达，再到 CP-SAT 的软约束优化——三者不是替代关系，而是层层递进的建模思路。

一句话概括：

排课的本质，是在海量 0-1 组合中，寻找一个既合法又尽量优秀的解。

一张看似普通的课程表背后，其实是一套严谨的数学建模、逻辑推理和智能搜索过程。