CP-SAT 的基本 API：构造约束所用的函数与写法

这一章讲什么

本章按用途列出 CP-SAT 常用的 API，每一项都配一个可以运行的示例。

• 变量的建立(整数、布尔、取值不连续)

• 线性约束与带条件的约束(only_enforce_if)

• 最大、最小、绝对值、乘、除、取余

• 逻辑约束(AND / OR / 恰好一个 / XOR)

• 允许与禁止的取值组合、数组元素引用(add_element)、逆映射(add_inverse)

各节都按“方法说明 + 可运行示例”排，示例的输出就是约束效果的直接证据。

from ortools.sat.python import cp_model
from helper.ortools import get_all_solutions, is_between, is_not_between

这一章用到的函数

下表按用途把 API 分了类，每个函数在正文里都配有示例，可以当作字典查阅；示例一律用 get_all_solutions() 取出全部解并排列出来，因此约束实际做了什么，看解就能明白，不必去猜。读的时候可以按表格查，也可以按小节顺序读。

分类	函数
创建变量	new_int_var, new_bool_var, new_int_var_from_domain
目标函数	minimize, maximize
线性约束	add, add_linear_constraint, add_linear_expression_in_domain
最大、最小、绝对值	add_min_equality, add_max_equality, add_abs_equality
乘、除、取余	add_modulo_equality, add_multiplication_equality, add_division_equality
互不相同的值	add_all_different
逻辑约束	add_implication, add_bool_or, add_at_least_one, add_at_most_one, add_exactly_one, add_bool_and, add_bool_xor
取值组合	add_allowed_assignments, add_forbidden_assignments
数组、元素	add_element, add_inverse

创建变量

• new_int_var：给出最小值和最大值，再给出变量名，就得到一个整数变量

• new_bool_var：建立最小值 0、最大值 1 的整数变量，参数只填变量名

• new_int_var_from_domain：取值范围不连续时用它

下面按这三个函数各给一个例子，例子里都用辅助函数 get_all_solutions() 把解全部取出，既能看清变量能取哪些值，也能确认每种写法的取值范围。

第一个例子是 \(0 \le x \le 3\) 的整数变量，它的取值范围是连续的四个整数，穷举出来的解就是这四个值。后面几个例子都按同样的方式检查。

model = cp_model.CpModel()
x = model.new_int_var(0, 3, 'x')
get_all_solutions(model)

[{'x': 0}, {'x': 1}, {'x': 2}, {'x': 3}]

第二个例子是布尔变量，其本质就是 \(0 \le b \le 1\) 的整数变量，取值范围只有 0 和 1。把解全部列出来，得到的也只有两组解，没有第三种可能。

model = cp_model.CpModel()
x = model.new_bool_var('b')
get_all_solutions(model)

[{'b': 0}, {'b': 1}]

候选值需要逐个指定时，就用 Domain.from_values()，它把给定的值组成一个取值域，而不必写成连续区间。取值域是一个集合，列出的顺序不影响结果。

model = cp_model.CpModel()
domain = cp_model.Domain.from_values([1, 3, 5, 7])
x = model.new_int_var_from_domain(domain, 'x')
get_all_solutions(model)

[{'x': 1}, {'x': 3}, {'x': 5}, {'x': 7}]

范围不止一段时，交给 Domain.from_flat_intervals() 来指定；每一段用两个连续的值(先下限、后上限)组成一对写进去。哪一头没有设界限，就用 INT_MIN 和 INT_MAX 顶上，这种写法比逐个列出取值简单得多。段与段之间的值被排除在外，因此这个写法适合跳开某些区间的场合。

model = cp_model.CpModel()
domain = cp_model.Domain.from_flat_intervals([1, 3, 7, 9, 10, 12])
x = model.new_int_var_from_domain(domain, 'x')
get_all_solutions(model)

[{'x': 1},
 {'x': 2},
 {'x': 3},
 {'x': 7},
 {'x': 8},
 {'x': 9},
 {'x': 10},
 {'x': 11},
 {'x': 12}]

线性约束

• add()：把线性表达式的比较式直接作为约束添加进去

• add_linear_constraint()：连同下限、上限一起给出，添加一条约束

• add_linear_expression_in_domain()：把线性表达式限制在不连续的取值范围里

下面两个例子做的都是 \(30 \le 10 x \le 50\) 这一条线性约束，差别只在写法：例 1 调用两次 add()，一次管下限，一次管上限；例 2 用 add_linear_constraint()，上下限一次说完，代码更短一些。写长式子时，后者更不容易漏掉某一侧。两种写法得到的约束完全相同，选择哪一种只取决于可读性。

model = cp_model.CpModel()
x = model.new_int_var(0, 100, 'x')
model.add(10 * x <= 50)
model.add(10 * x >= 30)
get_all_solutions(model)

[{'x': 3}, {'x': 4}, {'x': 5}]

model = cp_model.CpModel()
x = model.new_int_var(0, 100, 'x')
model.add_linear_constraint(10 * x, 30, 50)
get_all_solutions(model)

[{'x': 3}, {'x': 4}, {'x': 5}]

要把 \(30 \leq 10x \leq 50\) 或者 \(70 \leq 10x \leq 80\) 写成一条约束，就要用到 add_linear_expression_in_domain()。Domain.from_flat_intervals([30, 50, 70, 80]) 里摆的是两个区间，即 30 到 50 与 70 到 80，两段之间的取值被排除在外。同一段内的值仍然连续，因此这个写法省去了逐个列举。

model = cp_model.CpModel()
x = model.new_int_var(0, 100, 'x')
domain = cp_model.Domain.from_flat_intervals([30, 50, 70, 80])
model.add_linear_expression_in_domain(10 * x, domain)
get_all_solutions(model)

[{'x': 3}, {'x': 4}, {'x': 5}, {'x': 7}, {'x': 8}]

本书另外准备了两个辅助函数，它们生成的是比较式，用 add() 一加就成为约束，不必自己拼比较运算。否定式 is_not_between() 用来写“不在这个范围”的条件。

• \(l \le x \le u\)：is_between(x, l, u)

• \(x < l \lor x > u\)：is_not_between(x, l, u)

model = cp_model.CpModel()
x = model.new_int_var(1, 6, 'x')
y = model.new_int_var(1, 6, 'y')
model.add(is_between(x + y, 9, 10))
get_all_solutions(model)

[{'x': 3, 'y': 6},
 {'x': 4, 'y': 5},
 {'x': 4, 'y': 6},
 {'x': 5, 'y': 4},
 {'x': 5, 'y': 5},
 {'x': 6, 'y': 3},
 {'x': 6, 'y': 4}]

model = cp_model.CpModel()
x = model.new_int_var(1, 6, 'x')
y = model.new_int_var(1, 6, 'y')
model.add(is_not_between(x + y, 4, 11))
get_all_solutions(model)

[{'x': 1, 'y': 1}, {'x': 2, 'y': 1}, {'x': 1, 'y': 2}, {'x': 6, 'y': 6}]

条件分支

约束建好之后，调用 only_enforce_if() 就能指定它在什么条件下才生效。前提只能是布尔变量(一个或多个)，或者它们的否定，整数变量不能直接拿来当条件。例如要实现下面的条件，就需要中间垫一个布尔变量，把两个比较式拴在一起。

\[ 1 \leq x \leq 3, \quad 1 \leq y \leq 3 \]

\[\begin{split} z = \begin{cases} 50, & \text{if } x + y \geq 4 \\ -50, & \text{otherwise} \end{cases} \end{split}\]

代码里用 only_enforce_if(cond) 与 only_enforce_if(~cond) 两个方法，把 cond 挂到 x + y >= 4 上，再借这个条件去管 z 的取值。两个分支合起来覆盖全部情形，因此 z 在任何取值下都只有一个值。

model = cp_model.CpModel()
x, y = [model.new_int_var(1, 3, name) for name in 'xy']
z= model.new_int_var(-100, 100, 'z')

cond = model.new_bool_var('cond')
model.add(x + y >= 4).only_enforce_if(cond)
model.add(x + y < 4).only_enforce_if(~cond)

model.add(z == 50).only_enforce_if(cond)
model.add(z == -50).only_enforce_if(~cond)
get_all_solutions(model)

[{'x': 1, 'y': 1, 'z': -50, 'cond': 0},
 {'x': 2, 'y': 1, 'z': -50, 'cond': 0},
 {'x': 1, 'y': 2, 'z': -50, 'cond': 0},
 {'x': 1, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 2, 'y': 2, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 2, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 2, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 1, 'z': 50, 'cond': 1}]

上面那种写法要自己造比较式的否定，稍有疏忽就会写错。本书的辅助函数 equals(cond, expr, model) 承担了这一步：它自动生成 expr 的否定，再往 model 里添加两条约束。

model.add(expr).only_enforce_if(cond)
model.add(inverse_expr).only_enforce_if(~cond)

下面的代码用 equals() 把 x + y >= 4 这个条件挂到 cond 上。

from helper.ortools import equals
model = cp_model.CpModel()
x, y = [model.new_int_var(1, 3, name) for name in 'xy']
z= model.new_int_var(-100, 100, 'z')

cond = model.new_bool_var('cond')
equals(cond, x + y >= 4, model)

model.add(z == 50).only_enforce_if(cond)
model.add(z == -50).only_enforce_if(~cond)
get_all_solutions(model)

[{'x': 1, 'y': 1, 'z': -50, 'cond': 0},
 {'x': 2, 'y': 1, 'z': -50, 'cond': 0},
 {'x': 1, 'y': 2, 'z': -50, 'cond': 0},
 {'x': 1, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 2, 'y': 2, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 2, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 2, 'y': 3, 'z': 50, 'cond': 1},
 {'x': 3, 'y': 1, 'z': 50, 'cond': 1}]

这段代码约束的是两者中较小的那个：2 * x 与 y 的最小值等于 2。例如 x=1, y=3 时，min(2, 3) = 2，这一组取值满足约束，因此它是一个解。例子里只举一两个解，完整解集由示例输出给出。

model = cp_model.CpModel()
x, y = [model.new_int_var(0, 4, n) for n in 'xy']
model.add_min_equality(2, [2 * x,  y])
get_all_solutions(model)

[{'x': 1, 'y': 2},
 {'x': 1, 'y': 3},
 {'x': 1, 'y': 4},
 {'x': 2, 'y': 2},
 {'x': 3, 'y': 2},
 {'x': 4, 'y': 2}]

这段代码改为约束较大的那个：2 * x 与 y 的最大值等于 4。例如 x=2, y=3 时，max(4, 3) = 4，这样的组合同样是一个解。最小值与最大值各有一条约束，写法只差一个方法名。

model = cp_model.CpModel()
x, y = [model.new_int_var(1, 4, n) for n in 'xy']
model.add_max_equality(4, [2 * x, y])
get_all_solutions(model)

[{'x': 1, 'y': 4},
 {'x': 2, 'y': 1},
 {'x': 2, 'y': 2},
 {'x': 2, 'y': 3},
 {'x': 2, 'y': 4}]

这次考察的是绝对值：x - y 的绝对值必须等于 2。例如 x=3, y=1 时，|3 - 1| = 2，因此它是一个解；两个变量的取值对调之后，同样能得到一个解。绝对值约束把两个方向的取值合成一条，不必分情形讨论。

model = cp_model.CpModel()
x, y = [model.new_int_var(1, 4, n) for n in 'xy']
model.add_abs_equality(2, x - y)
get_all_solutions(model)

[{'x': 1, 'y': 3}, {'x': 2, 'y': 4}, {'x': 3, 'y': 1}, {'x': 4, 'y': 2}]

变量之间的乘法和除法

整数变量之间要写乘法、除法，有几个现成的方法可用，下面列出的三个都可以直接调用，目标变量由各自的方法确定，不必拆开手写。

• add_modulo_equality(target, dividend, divisor)：添加 dividend % divisor == target 这个约束

• add_multiplication_equality(target, *expressions)：添加 product(expressions) == target 这个约束

• add_division_equality(target, numerator, denominator)：添加 numerator // denominator == target 这个约束，即整数除法

这三个方法都要求目标变量事先建好，并且结果落在整数范围之内。

下面这段代码用 add_multiplication_equality() 找出三边长都是整数的直角三角形，也就是勾股数。

model = cp_model.CpModel()
max_n = 20
x, y, z = [model.new_int_var(1, max_n, n) for n in 'xyz']
x2, y2, z2 = [model.new_int_var(1, 2 * max_n**2, n) for n in ['x2', 'y2', 'z2']]
model.add_multiplication_equality(x2, x, x)
model.add_multiplication_equality(y2, y, y)
model.add_multiplication_equality(z2, z, z)
model.add(x2 + y2 == z2)
model.add(y >= x)
get_all_solutions(model)

[{'x': 3, 'y': 4, 'z': 5, 'x2': 9, 'y2': 16, 'z2': 25},
 {'x': 5, 'y': 12, 'z': 13, 'x2': 25, 'y2': 144, 'z2': 169},
 {'x': 6, 'y': 8, 'z': 10, 'x2': 36, 'y2': 64, 'z2': 100},
 {'x': 8, 'y': 15, 'z': 17, 'x2': 64, 'y2': 225, 'z2': 289},
 {'x': 9, 'y': 12, 'z': 15, 'x2': 81, 'y2': 144, 'z2': 225},
 {'x': 12, 'y': 16, 'z': 20, 'x2': 144, 'y2': 256, 'z2': 400}]

互不相同的值

要让一组变量彼此都不相等，有现成的 add_all_different(*expressions)。它给指定的所有表达式都加上“取值互不相同”这条约束，数独、分配问题这类要求各不相同的场合常用到它。下面的代码求的是 1, 2, 3 的排列，一共 6 种。这类约束比逐对写不等更省子句，求解器内部会利用它的结构。

model = cp_model.CpModel()
x, y, z = [model.new_int_var(1, 3, n) for n in 'xyz']
model.add_all_different(x, y, z)
get_all_solutions(model)

[{'x': 3, 'y': 2, 'z': 1},
 {'x': 3, 'y': 1, 'z': 2},
 {'x': 2, 'y': 3, 'z': 1},
 {'x': 2, 'y': 1, 'z': 3},
 {'x': 1, 'y': 3, 'z': 2},
 {'x': 1, 'y': 2, 'z': 3}]

逻辑约束

这一节的约束只接受布尔变量及其否定，整数变量不能直接用，写的时候要注意。

方法	内容
add_implication(a, b)	a ⇒ b，即 a 为真则 b 也为真
add_bool_or([a, b, c])	a OR b OR c，即至少 1 个为真
add_at_least_one([a, b, c])	至少 1 个为真
add_at_most_one([a, b, c])	最多 1 个为真
add_exactly_one([a, b, c])	恰好 1 个为真
add_bool_and([a, b, c])	a AND b AND c，即全部为真
add_bool_xor([a, b, c])	为真的变量个数是奇数

add_implication(a, b) 添加的是逻辑蕴含，含义就是 a 为真则 b 也为真。这条约束可以用下面这张表来说明。

输入 a	输入 b	输出 a → b
0	0	1
0	1	1
1	0	0
1	1	1

只有 a 为真而 b 为假时，输出 a → b 才为 0，其余三种组合都是 1。下面的代码去找输出 a → b 为 1 的解，一共得到 3 个解。

model = cp_model.CpModel()
a, b = [model.new_bool_var(n) for n in 'ab']
model.add_implication(a, b)
get_all_solutions(model)

[{'a': 0, 'b': 0}, {'a': 0, 'b': 1}, {'a': 1, 'b': 1}]

add_bool_or() 与 add_at_least_one() 含义相同：布尔变量列表中至少有一个为真，全部为假的那种组合被排除，因此这两个方法可以互换。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_bool_or(x, y, z)
get_all_solutions(model)

[{'x': 0, 'y': 1, 'z': 0},
 {'x': 0, 'y': 1, 'z': 1},
 {'x': 0, 'y': 0, 'z': 1},
 {'x': 1, 'y': 0, 'z': 1},
 {'x': 1, 'y': 0, 'z': 0},
 {'x': 1, 'y': 1, 'z': 0},
 {'x': 1, 'y': 1, 'z': 1}]

add_at_most_one() 管的是另一头：布尔变量列表中最多一个为真，也就是说两个以上同时为真的情况不会发生，用来表示“只能选一个”时很方便；与下一个方法一起看，两者的差别只在“至少一个”这一半。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_at_most_one(x, y, z)
get_all_solutions(model)

[{'x': 0, 'y': 0, 'z': 0},
 {'x': 0, 'y': 1, 'z': 0},
 {'x': 0, 'y': 0, 'z': 1},
 {'x': 1, 'y': 0, 'z': 0}]

add_exactly_one() 要求布尔变量列表中恰好一个为真，相当于把至少一个与最多一个两条约束合在一起。骨牌装箱那类问题里，每块骨牌与每一格都各要一条。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_exactly_one(x, y, z)
get_all_solutions(model)

[{'x': 0, 'y': 1, 'z': 0}, {'x': 0, 'y': 0, 'z': 1}, {'x': 1, 'y': 0, 'z': 0}]

add_bool_and() 要求布尔变量列表中的全部变量为真，列表里只要有一个为假，整条约束就不成立。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_bool_and(x, y, z)
get_all_solutions(model)

[{'x': 1, 'y': 1, 'z': 1}]

这条约束往往太强，直接使用会把列出的变量全部钉死为真，因此一般与 only_enforce_if() 配合使用。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_bool_and(x, y).only_enforce_if(~z)
get_all_solutions(model)

[{'x': 1, 'y': 1, 'z': 0},
 {'x': 1, 'y': 1, 'z': 1},
 {'x': 1, 'y': 0, 'z': 1},
 {'x': 0, 'y': 0, 'z': 1},
 {'x': 0, 'y': 1, 'z': 1}]

add_bool_xor() 数的是个数：布尔变量列表中为真的变量个数必须是奇数，为真个数为偶数的组合都会被排除。

model = cp_model.CpModel()
x, y, z = [model.new_bool_var(n) for n in 'xyz']
model.add_bool_xor(x, y, z)
get_all_solutions(model)

[{'x': 0, 'y': 1, 'z': 0},
 {'x': 0, 'y': 0, 'z': 1},
 {'x': 1, 'y': 0, 'z': 0},
 {'x': 1, 'y': 1, 'z': 1}]

取值组合的解

add_allowed_assignments() 加的是允许这一面：给指定的变量列出可取的组合，它们就只能在这些组合里挑选，列表里每个变量都被限制在特定的组合上，不在列表中的组合一个也不会出现。允许的组合写多了不要紧，求解器只会采用其中的一个。

下面的代码给 x 和 y 指定组合([5, 6] 和 [6, 7])，给 y 和 z 另指定一组([6, 8] 和 [7, 9])，然后求出允许的解。

model = cp_model.CpModel()
x, y, z = [model.new_int_var(1, 10, n) for n in 'xyz']
model.add_allowed_assignments([x, y], [[5, 6], [6, 7]])
model.add_allowed_assignments([y, z], [[6, 8], [7, 9]])
get_all_solutions(model)

[{'x': 5, 'y': 6, 'z': 8}, {'x': 6, 'y': 7, 'z': 9}]

要给计算式指定候选解，需要引入中间变量。下面代码里的 x_plus_y 与 y_plus_z 就是中间变量，分别存放 x + y 和 y + z。有了它们，add_allowed_assignments() 才能规定 x_plus_y 取 5 或 6、y_plus_z 取 6 或 7 这样的组合。当计算式复杂时，用中间变量指定候选解最简单。中间变量的取值范围要覆盖所有可能的计算结果，否则约束会无意中排除解。

model = cp_model.CpModel()
x, y, z = [model.new_int_var(1, 10, n) for n in 'xyz']
x_plus_y = model.new_int_var(-100, 100, 'x + y')
y_plus_z = model.new_int_var(-100, 100, 'y + z')
model.add(x_plus_y == x + y)
model.add(y_plus_z == y + z)
model.add_allowed_assignments([x_plus_y, y_plus_z], [[5, 6], [6, 7]])
get_all_solutions(model)

[{'x': 1, 'y': 4, 'z': 2, 'x + y': 5, 'y + z': 6},
 {'x': 2, 'y': 3, 'z': 3, 'x + y': 5, 'y + z': 6},
 {'x': 3, 'y': 2, 'z': 4, 'x + y': 5, 'y + z': 6},
 {'x': 4, 'y': 1, 'z': 5, 'x + y': 5, 'y + z': 6},
 {'x': 4, 'y': 2, 'z': 5, 'x + y': 6, 'y + z': 7},
 {'x': 3, 'y': 3, 'z': 4, 'x + y': 6, 'y + z': 7},
 {'x': 2, 'y': 4, 'z': 3, 'x + y': 6, 'y + z': 7},
 {'x': 5, 'y': 1, 'z': 6, 'x + y': 6, 'y + z': 7},
 {'x': 1, 'y': 5, 'z': 2, 'x + y': 6, 'y + z': 7}]

add_forbidden_assignments() 站的是相反的一面：把不允许出现的组合一一指定下来，它们就不会出现在解里。下面的代码对 x 与 y、y 与 z 这两对变量，把 1, 2、1, 3、2, 2 这几种组合全部禁掉，剩下的组合才可能成为解。允许与禁止是同一件事的两种说法，用哪一种取决于哪一边的组合更少。

model = cp_model.CpModel()
x, y, z = [model.new_int_var(1, 3, n) for n in 'xyz']
model.add_forbidden_assignments([x, y], [[1, 2], [1, 3], [2, 2]])
model.add_forbidden_assignments([y, z], [[1, 2], [1, 3], [2, 2]])
get_all_solutions(model)

[{'x': 3, 'y': 3, 'z': 1},
 {'x': 3, 'y': 2, 'z': 1},
 {'x': 3, 'y': 1, 'z': 1},
 {'x': 2, 'y': 1, 'z': 1},
 {'x': 2, 'y': 3, 'z': 1},
 {'x': 2, 'y': 3, 'z': 2},
 {'x': 2, 'y': 3, 'z': 3},
 {'x': 3, 'y': 3, 'z': 3},
 {'x': 3, 'y': 2, 'z': 3},
 {'x': 3, 'y': 3, 'z': 2},
 {'x': 1, 'y': 1, 'z': 1}]

数组元素

add_element(index, values, element) 用来表达数组 values 中第 index 个元素正好等于 element。可以用它在指定位置上固定数组中的某个元素，不需要逐个变量去写约束。索引本身也可以是变量，于是取哪一个也交给求解器决定。

model = cp_model.CpModel()
index = model.new_int_var(0, 4, 'index')
element = model.new_int_var(-100, 100, 'element')
model.add_element(index, [1, 3, 5, 7], element)
get_all_solutions(model)

[{'index': 0, 'element': 1},
 {'index': 1, 'element': 3},
 {'index': 2, 'element': 5},
 {'index': 3, 'element': 7}]

values 也可以是变量列表，并不限于常量列表，因此可以用它把变量之间的取值关系写出来，而不只是从常数表里挑一个。变量列表的情形下，被选中的元素由索引与其余约束共同决定。

model = cp_model.CpModel()
x, y, z =  [model.new_bool_var(n) for n in 'xyz']
index = model.new_int_var(0, 3, 'index')
element = model.new_int_var(-100, 100, 'element')
model.add_at_most_one([x, y, z])
model.add_element(index, [x, y, z], element)
get_all_solutions(model)

[{'x': 0, 'y': 0, 'z': 0, 'index': 0, 'element': 0},
 {'x': 0, 'y': 1, 'z': 0, 'index': 0, 'element': 0},
 {'x': 0, 'y': 0, 'z': 1, 'index': 0, 'element': 0},
 {'x': 0, 'y': 0, 'z': 1, 'index': 1, 'element': 0},
 {'x': 0, 'y': 0, 'z': 0, 'index': 1, 'element': 0},
 {'x': 0, 'y': 1, 'z': 0, 'index': 1, 'element': 1},
 {'x': 0, 'y': 0, 'z': 1, 'index': 2, 'element': 1},
 {'x': 0, 'y': 0, 'z': 0, 'index': 2, 'element': 0},
 {'x': 0, 'y': 1, 'z': 0, 'index': 2, 'element': 0},
 {'x': 1, 'y': 0, 'z': 0, 'index': 2, 'element': 0},
 {'x': 1, 'y': 0, 'z': 0, 'index': 1, 'element': 0},
 {'x': 1, 'y': 0, 'z': 0, 'index': 0, 'element': 1}]

add_inverse(a, b) 用数组 a 的索引去决定数组 b 的元素，具体约束的是 b[a[i]] == i，这样一来，b 必定与 a 的 arg_sort() 对得上，两者互为逆映射。

例如当 a 的元素是 [1, 2, 0] 时，索引按 [2, 0, 1] 的顺序把对应的元素放进数组 b，这样就得到 b[1] == 0, b[2] == 1, b[0] == 2。逆映射在排列与坐标对应这类问题里很好用，写一次就能代替一组等式。

import numpy as np

model = cp_model.CpModel()
a = [model.new_int_var(0, 2, n) for n in ['a0', 'a1', 'a2']]
b = [model.new_int_var(0, 2, n) for n in ['b0', 'b1', 'b2']]
model.add_inverse(a, b)
for sol in get_all_solutions(model):
    a_sol = [sol[f'a{i}'] for i in range(3)]
    b_sol = [sol[f'b{i}'] for i in range(3)]
    print(f'a = {a_sol}, b = {b_sol}, arg_sort = {np.argsort(a_sol).tolist()}')

a = [2, 1, 0], b = [2, 1, 0], arg_sort = [2, 1, 0]
a = [1, 2, 0], b = [2, 0, 1], arg_sort = [2, 0, 1]
a = [2, 0, 1], b = [1, 2, 0], arg_sort = [1, 2, 0]
a = [1, 0, 2], b = [1, 0, 2], arg_sort = [1, 0, 2]
a = [0, 2, 1], b = [0, 2, 1], arg_sort = [0, 2, 1]
a = [0, 1, 2], b = [0, 1, 2], arg_sort = [0, 1, 2]

小结

想做的事	用的函数
整数变量	new_int_var(lb, ub, name)
0/1 变量	new_bool_var(name)
只用离散的值	new_int_var_from_domain(Domain.from_values([...]), name)
区间的集合	Domain.from_flat_intervals([lb1, ub1, lb2, ub2])
上下限一起设	add_linear_constraint(式, lb, ub)
收进不连续的范围	add_linear_expression_in_domain(式, domain)
有条件地让约束生效	model.add(...).only_enforce_if(b)
最大、最小、绝对值	add_max_equality / add_min_equality / add_abs_equality
积、商、余数	add_multiplication_equality / add_division_equality / add_modulo_equality
全部不同	add_all_different
允许、禁止组合	add_allowed_assignments / add_forbidden_assignments
引用数组	add_element(index, values, element)
逆映射	add_inverse(a, b)，约束为 b[a[i]] == i

• 约束做的事，本质上就是不断排除不可能的取值组合，用 get_all_solutions() 把解集全部列出来看，它的含义就清楚了

• 逻辑约束只接受布尔变量；要用整数，先把比较式挂到一个布尔变量上，或者用本章的辅助函数代劳