约束满足问题(CSP)：给每个变量定一个值，让全部条件都满足

约束满足问题(CSP)：给每个变量定一个值，让全部条件都满足#

这一章讲什么#

这一章讨论约束满足问题(Constraint Satisfaction Problem，简称 CSP)，先给出这一类问题的定义，再比较穷举与 Z3 两种解法的差别。

  • 约束满足问题的定义与两个要素(变量、约束)

  • 穷举的计算量随规模增长的情况

  • Z3 求解约束的方式

三节按这个顺序展开：先给出定义，再说明穷举的代价，最后看 Z3 如何用约束替代逐条试错。全章只用到两个关键词：变量与约束；后面各节的写法虽有不同，处理的对象始终不变。

什么是约束满足问题#

所谓约束满足问题，就是给若干变量各定一个值，使这些值满足给定条件(约束)的问题，先看一个小例子。

5 个小朋友(A、B、C、D、E)一个接一个吃完了便当。 请根据下面两句话，把他们吃完的先后顺序排出来。

  • A 比 B 吃得晚，但比 C 吃得早。

  • D 比 E 吃得早，但比 C 吃得晚。

在这个问题里，变量与约束这两个部分立刻显现出来。

  • 变量：5 个人各自“第几个吃完”

  • 约束：“A 在 B 之后”“A 在 C 之前”这类条件

这两栏在任何一题里都存在：哪些值还没有确定下来，哪些条件必须同时成立。把 5 个人的顺序排定，回头逐条检查，一条也没有违反，这个排列就是答案。题目本身并不难，但它把约束满足问题的两个要素完整地呈现了出来，后面的各种谜题都是这两个部分的组合。

把条件写成符号#

由于日常语言的写法不容易推想，我们换成符号再写一遍，写出来的式子与原来的两句话完全等价。

记 \(X \prec Y\) 为“X 比 Y 先吃完”，这种写法在纸上和程序里都好用。

  1. A 比 B 晚、比 C 早 → \(B \prec A \prec C\)

  2. D 比 E 早、比 C 晚 → \(C \prec D \prec E\)

两条一接，就串成 \(B \prec A \prec C \prec D \prec E\) 这一条链，这样，要找的目标就变得很具体：满足这个先后顺序的那个排列。换成符号之后，几条短链能直接接成长链，传递关系不必自己推。写成的式子也可以原样搬进程序，不必再翻译一次。

先用最直接的办法：全部试一遍#

最直接的做法，是把可能的顺序全部列出来，再逐条筛掉不合格的，这叫做穷举，也叫全数探索。它的代价可以先算出来：候选有 \(n!\) 个，每个都要与全部约束核对一遍。

5 个人排成一列，总共只有 \(5! = 120\) 种，即使一种一种试，也是一瞬间就能完成的事。

from itertools import permutations

kids = ["A", "B", "C", "D", "E"]

# order 是“按吃完顺序排列的小孩编号”
for order in permutations(range(len(kids))):
    rank = {kids[i]: pos for pos, i in enumerate(order)}   # 每个小孩的名次
    if rank["B"] < rank["A"] < rank["C"] and rank["C"] < rank["D"] < rank["E"]:
        print(" → ".join(kids[i] for i in order))

B → A → C → D → E

筛完之后，只剩 B → A → C → D → E 这一个顺序。

5 个人是一瞬间的事，人数增加以后情况就不同了：排列的数目按 \(n!\) 增长，每多一个人就翻上几倍，很快就无法应付。

import math

for n in [5, 8, 10, 12]:
    print(f"{n:2d} 人: {math.factorial(n):,} 种")

 5 人: 120 种
 8 人: 40,320 种
10 人: 3,628,800 种
12 人: 479,001,600 种

12 个人大约有 4 亿 8 千万种排法，即使每秒能试 100 万种，也要花上 8 分钟；而再增加到 20 个人(约 2.4×10¹⁸ 种)，就根本等不到结果了。

“全部试一遍”这条路，人数稍微增加几个就走不通了。这一章的后半部分，我们看 Z3 如何绕过这堵墙。

补充：itertools.permutations 的用法#

穷举时用到的 permutations()，作用是把给定的元素按各种顺序全部排列一遍。下面给出它的调用形式。

itertools.permutations(iterable, r=None)

  • iterable：要排列的元素

  • r：一次取出几个(省略时全部取出)

给三个元素，得到的就是 \(3! = 6\) 种排列，可见元素一多，数目立刻就不够用了。这个函数不替调用者剪枝：每一种顺序都会被造出来，合不合格要自己筛。

for p in permutations(["A", "B", "C"]):
    print(p)

('A', 'B', 'C')
('A', 'C', 'B')
('B', 'A', 'C')
('B', 'C', 'A')
('C', 'A', 'B')
('C', 'B', 'A')

使用 permutations() 时，有三件事需要注意。

  1. 顺序算作不同：(A, B) 与 (B, A) 是两个不同的结果。

  2. 它不处理重复：元素中本来就有相同的，同一个排列会出现多次。

  3. 计算量是 \(n!\)：元素一多，数目就急剧增长。

第二条最容易被忽略：元素按位置区分，同一个排列会出现多次，计数时不能直接当作互不相同的结果。小问题的答案可以用它核对，用眼睛确认即可；规模一大就不能依赖它，这时该把工作交给求解器。

换一个工具：Z3#

Z3 属于约束求解器一类，把条件原样写进去，它会自己找出能够同时满足这些条件的那一组取值，其做法与穷举正好相反。

各自要做的事

穷举

把候选全部列出，一个一个验证

Z3

只把条件写清楚，寻找的工作交给它

无论解什么题，用 Z3 的步骤都是同样的三步，后面几章一直沿用。约束交进去之后，Z3 不必把候选一个个试过来。它把条件翻译成逻辑公式，交给内部的求解内核，由内核判断哪些取值可以同时成立。

  1. 建立变量

  2. 添加约束

  3. 取出解

from z3 import IntVector, Solver, Distinct, sat

kids = ["A", "B", "C", "D", "E"]

# 表示每个小孩“吃完的名次”的 5 个整数变量（pos[0] 是 A，pos[1] 是 B …）
pos = IntVector("pos", 5)
eat_a, eat_b, eat_c, eat_d, eat_e = pos

solver = Solver()

# 1. 名次是 0 到 4 中的一个
for p in pos:
    solver.add(p >= 0, p < len(kids))

# 2. 没有名次相同的小孩
solver.add(Distinct(pos))

# 3. 问题的条件  B ≺ A ≺ C ≺ D ≺ E
solver.add(eat_b < eat_a, eat_a < eat_c)
solver.add(eat_c < eat_d, eat_d < eat_e)

# 4. 取出解，按名次从小到大排列
if solver.check() == sat:
    model = solver.model()
    rank = {kid: model[pos[i]].as_long() for i, kid in enumerate(kids)}
    print(" → ".join(sorted(kids, key=lambda kid: rank[kid])))

B → A → C → D → E

算出来的答案与穷举完全相同，这里值得停下来，看可搜索的范围如何逐层收窄。

  1. 只建立 IntVector("pos", 5)，值可以任意取 → 无限

  2. 补上 0 <= p < 5 → \(5^5 = 3125\) 种

  3. 再补上 Distinct(pos) → \(5! = 120\) 种(与穷举站在同一条线上)

  4. 最后补上 \(B \prec A \prec C \prec D \prec E\) → 1 种

穷举从第 3 步那个范围开始，剩下的候选要逐条验证；Z3 则相反，先把条件写全，注定不合格的候选从一开始就不去构造。这四步里，范围只会缩小，不会扩大：每加一条约束，可行解的集合就是上一步的子集。人数再多，做法还是这一套。

小结#

手法

计算量

适合的情形

itertools.permutations

\(O(n!)\)

小问题，用眼睛核对

Z3

从条件出发高效搜索

条件复杂、人数较多的题

  • 约束满足问题由“变量”和“约束”两部分构成，两者缺一不可

  • 穷举的计算量是 \(n!\)，规模稍微一大就不能用了

  • Z3 能照原样收下约束，题目换了也不必改框架