Z3的用法：用五个步骤解约束，从建立变量到取出全部解

Z3的用法：用五个步骤解约束，从建立变量到取出全部解#

这一章讲什么#

上一章已经看到，用 Z3 处理约束满足问题，代码可以写得非常短。这一章按 Z3 的基本流程依次说明它的用法，下面先列出要点。

  • 用 Z3 解问题的五个步骤

  • Z3 的变量与普通 Python 数值的差别

  • 从模型(也就是答案)中取出变量值的方法

  • 例题：SEND + MORE = MONEY

  • 列出全部解的方法

这一章的代码请从上往下依次执行，前面的代码中建立的变量，后面的代码还要继续使用。五个步骤的顺序不能颠倒：变量先于约束，约束先于求解，取值必须在 check() 返回 sat 之后。

from z3 import *

用 Z3 解题的流程#

无论解什么题，用 Z3 的步骤几乎都一样。

步骤

要做的事

用到的工具

1

建立变量

Int, Ints, IntVector

2

准备求解器

Solver()

3

添加约束

solver.add()

4

询问有没有解

solver.check()

5

取出值

solver.model()

下面按顺序看这五个步骤，其中前两步只是准备工作，真正求解的是第三、四步。

第1步：建立变量#

先要有变量，用来存放还没有确定下来的值。Z3 提供三种建立整数变量的方法，用哪一种都可以，三种方法建出来的变量一样，区别只在一次声明几个变量。实际写代码时，要建几个变量往往事先知道，Ints() 与 IntVector() 可以一次声明多个，比逐个调用 Int() 简洁，三者在约束中完全等价。

x = Int("x")             # 创建一个整数变量
y, z = Ints("y z")       # 用空格分隔名字，一次创建多个
v = IntVector("v", 5)    # v[0] 〜 v[4] 共 5 个整数变量

这样建出来的变量，其类型为 ArithRef，而 IntVector 本身是一个 Python 列表，其中存放的元素也都是 ArithRef。因此可以像普通列表那样遍历，这层关系在后面的索引操作里会经常用到。

print(type(x), x, y, z)
print(type(v), type(v[0]), v)

<class 'z3.z3.ArithRef'> x y z
<class 'list'> <class 'z3.z3.ArithRef'> [v__0, v__1, v__2, v__3, v__4]

Z3 的变量与普通的 Python 数值不同：由于它的值还没有确定，因此对它作运算得不到数值，结果仍以表达式的形式保留下来。如果变量一开始就有具体数值，x + 1 会立刻算出一个数，约束也就无从表达。把运算留成表达式的形式，求解器才能在未知的取值上做推理。

print(x + 1)            # 不会计算，原样显示为表达式
print(x + 1 == 10)      # 变成条件式（BoolRef）
print(type(x + 1 == 10))

x + 1
x + 1 == 10
<class 'z3.z3.BoolRef'>

第2步：准备求解器#

约束要有一个地方存放，还需要有工具负责寻找解，这个角色由 Solver 担任。开始时先建立一个空的求解器，后面的约束都加在它身上，建立求解器的写法很简单，一行即可。

solver = Solver()
print(type(solver), solver)   # [] 表示「还没有任何约束」

<class 'z3.z3.Solver'> []

第3步：添加约束#

约束通过 solver.add() 交给求解器，而 ==、<、>、+ 这些运算符写出来，本身就是约束表达式。一次添加一条约束也可以，收集成列表一次添加进去也可以，例如一次添加两条，与分两次调用的效果完全相同。两种写法的差别只在代码组织：add() 接受任意多条约束，也接受可迭代对象，加进去的约束之间是合取关系，必须同时成立。

solver = Solver()

constraints = [
    x + y == 10,   # x 与 y 之和是 10
    x > 0,         # x 是正数
    y > 0,         # y 是正数
]
solver.add(*constraints)   # 展开列表传入（等同于 solver.add(a, b, c)）
print(solver)

[x + y == 10, x > 0, y > 0]

把 solver 交给 print()，它会把当前装入的约束全部显示出来。注意，这一步打印的是求解器此刻持有的所有约束，并不影响求解结果；要核对条件有没有写错，看这份输出即可。输出中约束的先后由内部结构决定，与添加顺序不一定相同，因此它适合核对内容，不适合逐行比对。

第4步：询问有没有解#

Solver.check() 问的就是这一件事：满足这些约束的解是否存在。它返回的结果有三种，分别表示三种不同的状态，看返回值的名字就能明白。

返回值

含义

sat

找到解了(satisfiable)

unsat

这样的解不存在(unsatisfiable)

unknown

判断不出来(超时，或者掺进了 Z3 不擅长的表达式)

 
if solver.check() == sat:
    print("有解")
else:
    print("无解")

有解

第5步：从模型中取出值#

有解的时候，调用 solver.model() 可以取出具体的数值。它返回的是一个 ModelRef 对象，其中装着每个变量对应的值，这个对象在后面的例子中会反复用到。

if solver.check() == sat:
    model = solver.model()
    print("x =", model[x])
    print("y =", model[y])
else:
    print("无解")

x = 9
y = 1

model[x] 得到的是 Z3 的 IntNumRef 类型，它表示 Z3 内部的整数常量，不能直接当作 Python 整数参与计算，需要先调用 as_long() 转换一次，把它变成普通的 Python 整数。IntNumRef 参与算术时不会自动变成 int，得到的仍是 Z3 的表达式，因此凡是要参与 Python 计算的地方，都要先转换。

print(type(model), type(model[x]))

print("x =", model[x].as_long())
print("x + y =", model[x].as_long() + model[y].as_long())

<class 'z3.z3.ModelRef'> <class 'z3.z3.IntNumRef'>
x = 9
x + y = 10

例题：SEND + MORE = MONEY#

用 OrTools 解同一个问题

这道题属于把字母换成数字的谜题，称为字母算术(Cryptarithm)。答案是 \(9567 + 1085 = 10652\)，下面验证 Z3 能否算出这个答案，解法不必另找，就是这一章讲的五个步骤，只是把五步串在一起。

S、E、N、D、M、O、R、Y 分别代表 0〜9 中不同的数字。

\[SEND + MORE = MONEY\]

请找出使这个式子成立的数字组合。

  1. 把 S、E、N、D、M、O、R、Y 声明为整数变量

  2. 添加约束：每个字母都在 0〜9 之间，并且彼此不同

  3. 把单词写成算式：\(SEND = 1000S + 100E + 10N + D\)

  4. 把 \(SEND + MORE = MONEY\) 作为约束添加进去

  5. 用 check() 和 model() 取出解

# 把 S, E, N, D, M, O, R, Y 设为整数变量
S, E, N, D, M, O, R, Y = Ints("S E N D M O R Y")
letters = [S, E, N, D, M, O, R, Y]

solver = Solver()

# 1. 每个字母都是 0〜9 之一
for letter in letters:
    solver.add(0 <= letter, letter <= 9)

# 2. 字母不同，数字也不同
solver.add(Distinct(letters))

# 3. 把单词写成算式  例：SEND = 1000*S + 100*E + 10*N + D
send = 1000*S + 100*E + 10*N + D
more = 1000*M + 100*O + 10*R + E
money = 10000*M + 1000*O + 100*N + 10*E + Y

# 4. SEND + MORE = MONEY
solver.add(send + more == money)

# 5. 最高位不能是 0
solver.add(S != 0, M != 0)

if solver.check() == sat:
    model = solver.model()
    print({str(letter): model[letter].as_long() for letter in letters})
    print(f"{model.eval(send)} + {model.eval(more)} = {model.eval(money)}")
else:
    print("无解")

{'S': 9, 'E': 5, 'N': 6, 'D': 7, 'M': 1, 'O': 0, 'R': 8, 'Y': 2}
9567 + 1085 = 10652

答案只有一种，整段代码中只用了两个运算符。

运算符

作用

例子

And

让所有条件同时成立

And(x > 0, y > 0)

Distinct

使给定的变量取值彼此不同

Distinct(a, b, c)

取出值也有两种写法，两者都以已经求出的模型为前提，对同一个模型反复取值不会改变模型本身。

  • model[x] … 取出变量的值

  • model.eval(式) … 取出整个表达式的计算结果

模型里装着什么#

ModelRef 是把变量和它的值放在一起的对象。往 [] 中传入变量，得到的是它的值；传入下标，得到的是变量的声明，两者不能混用。这种区别来自 Z3 的内部表示：变量被当作没有参数的函数，变量本身是一次函数应用，声明才是那个函数符号。

传入

返回

变量(ArithRef)

它的值(IntNumRef)

下标(整数)

变量的声明(FuncDeclRef)

 
print(model[0], type(model[0]))   # 第 0 个变量的「声明」

decl = model[0]
print(decl(), type(decl()))       # 加上 () 就变成变量（ArithRef）

S <class 'z3.z3.FuncDeclRef'>
S <class 'z3.z3.ArithRef'>

FuncDeclRef 是变量的声明，在其后面补上一对 ()，才变回变量本身。至于哪个字母排在第 0 位，取决于 Z3 内部的顺序，每次执行的结果可能都不一样。理清这个机制之后，就可以把模型中所有变量的值一次全部取出。

{str(decl): model[decl].as_long() for decl in model}

{'S': 9, 'O': 0, 'N': 6, 'R': 8, 'E': 5, 'M': 1, 'Y': 2, 'D': 7}

列出全部解#

需要的是“全部解”而不是“一个解”时，做法是每找到一个解，就添加一条“这个解不能再出现”的约束，然后继续调用 check()。因此这是一个逐次排除、反复求解的过程。循环在 check() 返回 unsat 时结束；如果约束本身不可满足，第一次调用就返回 unsat，此时一个解也取不到。

  1. 调用 check()，看还有没有解

  2. 有解就用 model() 取出来

  3. 添加“刚才那个解不要再给”的约束，回到第 1 步

  4. 直到没有解(unsat)，结束

随着解被一条条排除，每次调用 check() 都要重新搜索一遍，因此解多时总耗时大致按解的数量累加。

abc = Ints("a b c")
solver = Solver()

for n in abc:
    solver.add(1 <= n, n <= 3)   # 都在 1〜3 之间
solver.add(Distinct(abc))        # 三个数互不相同

while solver.check() == sat:
    model = solver.model()
    print(model)
    # 禁止与刚找到的解「完全相同」的组合
    solver.add(Not(And([decl() == model[decl] for decl in model])))

[c = 2, b = 3, a = 1]
[a = 3, c = 1, b = 2]
[c = 2, b = 1, a = 3]
[c = 1, b = 3, a = 2]
[c = 3, a = 2, b = 1]
[a = 1, c = 3, b = 2]

Not(And(c1, c2, ...)) 与 Or(Not(c1), Not(c2), ...) 含义相同，即“任意一项不同就可以”，落到约束上就是“不再给出与刚才相同的解”。

下面这一行代码也能做到同一件事。

solver.add(Or([decl() != model[decl] for decl in model]))

只不过这种写法每找出一个解就要调用一次 check()，解一多耗时就相当可观，因此需要注意。

小结#

用 Z3 解题，永远是这五个步骤。

  1. 建立变量(Int, Ints, IntVector)

  2. 建立 Solver()

  3. 用 solver.add() 添加约束

  4. 用 solver.check() 检查结果是 sat、unsat 还是 unknown

  5. 用 solver.model() 取值，再用 as_long() 转换成 Python 整数

  • Z3 的变量装的是“还没有确定下来的值”，因此在程序中始终以表达式的形式存在

  • 用 print(solver) 把约束逐条列出，写错的地方往往很容易发现

  • 想要全部解，就补上禁止已找到解的约束，一轮一轮重复，直到没有解为止