插入运算符凑出 99：让 Z3 决定括号的位置#
本章的内容#
数的顺序已经固定，要在相邻的数之间插入 +、-、*，再用括号改变运算顺序。
反复执行把相邻的两个数算成一个，就能表达任何加括号的方式
把每一层的数组都做成 Z3 的变量，用
If选择运算最后把找到的步骤还原成算式
与数的顺序可以自由调换的 24 点问题相比，区别在于：数序固定之后，排列那一整块约束消失，变量只剩每一层的位置与运算符。
对下面的式子，在
?处填入+、-、*中的某一个，并适当地加括号，使式子的值为 99。
1 ? 2 ? 3 ? 4 ? 5 ? 6 ? 7 ? 8 ? 9 = 99
思路#
不要把一个一个数顺着算下去，而是反复执行把相邻的两个算成一个的操作，直到只剩一个数为止。
例如从 1 2 3 4 5 出发，
计算
3 + 4，得到1 2 7 5计算
1 * 2，得到2 7 5计算
7 + 5，得到2 12计算
2 - 12，得到-10
这样每做一层，数就减少一个，最后剩下的那个数就是式子的值。反复合并相邻两项，正好对应一棵二叉树自底向上的构造，因此任何一种加括号的方式都能被这一串操作写出来。
graph
a1[1]
a2[2]
a3[3+4]
a4[5]
b1[1*2]
b2[3+4]
b3[5]
c1[1*2]
c2[3+4-5]
d1[1*2+3+4-5]
1 --> a1
2 --> a2
3 --> a3
4 --> a3
5 --> a4
a1 --> b1
a2 --> b1
a3 --> b2
a4 --> b3
b1 --> c1
b2 --> c2
b3 --> c2
c1 --> d1
c2 --> d1
只要让 Z3 决定在哪一处用哪个运算符合并，就等于把所有的加括号方式都试过了，不必真的把括号的写法一一列举出来。共 \(n-1\) 层，每一层可选的位置数是当时的元素个数减 1。
逐层计算#
把第 l 层的数组记为 f[l]，最初一层 f[0] 是 [1, 2, …, 9]，每做一层就短一个元素。
calc_tree(f, locs, ops) 把每一层的计算写成约束。在第 l 层选择位置 p = locs[l-1] 时，
i < p：f[l][i] == f[l-1][i]，即原样留下i == p：f[l][p] == f[l-1][p] op f[l-1][p+1]，即在这里计算i > p：f[l][i] == f[l-1][i+1]，即从左边错一位留下
这三条覆盖了第 l 层的每一个下标，因此每一层的值都被唯一确定。
from z3 import *
from helper.z3 import all_solutions
OP_SYMBOLS = '+-*' # 0:+, 1:-, 2:*
def calc_op(x1, x2, op):
"""按 op 的编号选择加、减、乘"""
return If(op == 0, x1 + x2, If(op == 1, x1 - x2, x1 * x2))
def calc_tree(f, locs, ops):
"""把每个阶段的计算整理成约束列表返回"""
exprs = []
for l in range(1, len(f)):
prev = f[l - 1]
for i in range(len(f[l])):
exprs.extend([
Implies(i < locs[l - 1], f[l][i] == prev[i]),
Implies(i == locs[l - 1], f[l][i] == calc_op(prev[i], prev[i + 1], ops[l - 1])),
Implies(i > locs[l - 1], f[l][i] == prev[i + 1]),
])
return exprs
用 If 选择运算符#
If(op == 0, x1 + x2, If(op == 1, x1 - x2, x1 * x2))
把 If(条件, 真时的值, 假时的值) 嵌套起来，切换三种运算。
|
计算 |
|---|---|
0 |
|
1 |
|
2 |
|
条件一多嵌套就深，因此选项较多时用 Function 更好读；本章只有三个，用 If 就足够。嵌套的 If 在约束里是一串条件式，读的时候要一层层往下对照。
显示成算式#
Z3 给出的是数，因此需要一套还原成算式的机制。Expr 是一个持有左式、运算符与右式的小类，它的 output() 沿着各层的步骤拼出字符串，缺的括号由它自己补上。
当 * 或 - 的右侧出现 + 或 -，或者 * 的左侧出现 + 或 - 时，要加上括号，以便把 1 + 2 * 3 与 (1 + 2) * 3 区分开。输出要能被 Python 重新解析，因此只在优先级不足以表达原结构的地方补括号。
class Expr:
"""把计算树变成带括号的字符串"""
def __init__(self, left, op, right):
self.left = left
self.op = op
self.right = right
def __str__(self):
# 左侧：* 的左边是 + - 时要加括号
if isinstance(self.left, Expr) and self.op == '*' and self.left.op in '+-':
left = f'({self.left})'
else:
left = f'{self.left}'
# 右侧：* 或 - 的右边是 + - 时要加括号
if isinstance(self.right, Expr) and self.op in '*-' and self.right.op in '+-':
right = f'({self.right})'
else:
right = f'{self.right}'
return f'{left} {self.op} {right}'
def output(numbers, locs, ops):
"""从数的顺序和步骤生成算式字符串"""
exprs = [str(x) for x in numbers]
for loc, op in zip(locs, ops):
exprs[loc] = Expr(exprs[loc], OP_SYMBOLS[op], exprs[loc + 1])
del exprs[loc + 1]
return str(exprs[0])
用小例子确认#
对 1 2 3 4 5 施加一个给定的步骤。
第 1 层：位置 2 取
+，即3 + 4第 2 层：位置 0 取
*，即1 * 2第 3 层：位置 1 取
-，即7 - 5第 4 层：位置 0 取
+，即2 + 2
结果应当是 1 * 2 + ((3 + 4) - 5) = 4。
n = 5
f = [[Int(f'f{l}_{i}') for i in range(n - l)] for l in range(n)]
solver = Solver()
for i in range(n):
solver.add(f[0][i] == i + 1) # 一开始是 1, 2, 3, 4, 5
locs = [2, 0, 1, 0] # 合并哪个位置
ops = [0, 2, 1, 0] # +, *, -, +
solver.add(calc_tree(f, locs, ops))
assert solver.check() == sat
m = solver.model()
expr = output([i + 1 for i in range(n)], locs, ops)
print(expr, "=", eval(expr))
print("各阶段的值")
for level in range(n):
print([m[f[level][i]] for i in range(n - level)])
1 * 2 + 3 + 4 - 5 = 4
各阶段的值
[1, 2, 3, 4, 5]
[1, 2, 7, 5]
[2, 7, 5]
[2, 2]
[4]
与手算一致，得到 1 * 2 + 3 + 4 - 5 = 4，按计算树来写就是 1 * 2 + ((3 + 4) - 5)。各层的元素个数也逐层减少。
寻找等于 99 的组合#
这一回让 Z3 决定位置与运算符，共有九个数，因此约束是位置 locs[i] 不小于 0 且小于 9-i-1，运算符取 0〜2，编号的含义与上一章相同。上界要减 1，是因为合并需要相邻两项：第 i 层还剩 9-i 个数，位置最大只能到倒数第二个。
n = 9
f = [[Int(f'f{l}_{i}') for i in range(n - l)] for l in range(n)]
solver = Solver()
for i in range(n):
solver.add(f[0][i] == i + 1) # 从 1 到 9
locs = IntVector('loc', n - 1) # 各阶段合并的位置
ops = IntVector('op', n - 1) # 各阶段的运算符
for i, loc in enumerate(locs):
solver.add(0 <= loc, loc < n - i - 1) # 到该阶段元素个数 - 1 为止
for op in ops:
solver.add(0 <= op, op <= 2) # 0:+, 1:-, 2:*
solver.add(calc_tree(f, locs, ops))
solver.add(f[-1][0] == 99) # 最后剩下的数是 99
print(solver.check())
m = solver.model()
print("各阶段的值")
for level in range(n):
print([m[f[level][i]] for i in range(n - level)])
locs_used = [m[x].as_long() for x in locs]
ops_used = [m[x].as_long() for x in ops]
print("位置:", locs_used)
print("运算符:", [OP_SYMBOLS[x] for x in ops_used])
sat
各阶段的值
[1, 2, 3, 4, 5, 6, 7, 8, 9]
[1, 2, -1, 5, 6, 7, 8, 9]
[1, 2, -1, 5, 6, 7, 17]
[1, 2, -1, 5, 6, 119]
[1, 2, -1, 5, -113]
[1, 3, 5, -113]
[1, 15, -113]
[1, -98]
[99]
位置: [2, 6, 5, 4, 1, 1, 1, 0]
运算符: ['-', '+', '*', '-', '-', '*', '+', '-']
最后把找到的步骤还原成算式，便于核对结果。还原用的是求解器给出的位置与运算符，因此算式与约束描述的步骤完全一致。
expr = output(list(range(1, 10)), locs_used, ops_used)
print(expr, "=", eval(expr))
1 - ((2 - (3 - 4)) * 5 + 6 - 7 * (8 + 9)) = 99
例如会得到下面这样的式子。
1 - ((2 - (3 - 4)) * 5 + 6 - 7 * (8 + 9)) = 99
Z3 找出的是满足条件的第一个解，因此式子的形状未必每次都相同，但结果都是 99。
小结#
数序固定时，加括号的方式可以表示成把相邻两个合并的操作序列
每一层各准备一个数组，用
calc_tree()把留下、计算、错位三种情形写成Implies运算符换成整数编号，用
If切换计算找到的步骤还原成计算树
Expr之后，就能当算式读数序也可以自由调换的 24 点问题，会多出一条排列的约束，即前一章