24 点：寻找四个数与三个运算符的组合

24 点：寻找四个数与三个运算符的组合#

本章的内容#

本章用 Z3 解「24 点」这道谜题：四个数、三个运算符，加上运算顺序，共同决定一个算式。

  • 四个数的排列用排列的约束来表达，即使有重复的数也能正确工作

  • 中间结果会出现分数，因此变量要取 Real，即实数

  • 运算符用 0〜5 的整数表示，再用 Implies 写出该编号对应的计算

同一个问题还会用 Function() 再写一种表示。

问题#

用四个数与 +、-、*、/ 与括号，组成一个值为 24 的式子。

例如 [1, 5, 5, 5] 时

(5 - (1 / 5)) * 5 = 24

这就是一个满足条件的算式，而数的排列有 \(4! = 24\) 种，有重复的数时相应减少，运算符的选法有 \(6^3\) 种，具体取法后面会说明。两者相乘，最多有 \(24 \times 216 = 5184\) 种组合，这个数目用纸笔逐一核对并不现实，因此交给 Z3 去搜索。

用约束表达数的排列#

solve_24 中希望把四个数当成排好序的一组来用，因此要写出排列的约束。

permutation(xs, values) 返回一组约束，使 xs 成为 values 的一个排列。返回的是约束列表，需要逐条交给求解器，而不是在 Python 里真的去重排数组。

  1. xs 的每个元素都取自 values 中出现的值

  2. 对每个值 v，xs 中出现的次数与 values 中的次数相同

以 [1, 5, 5, 5] 为例，就是 1 出现 1 次、5 出现 3 次；与使用 Distinct() 的写法不同，这种做法在有重复的数时也能正确处理，因为 Distinct() 要求两两不同，只适合四个数互不相同的情形。

from z3 import *
from helper.z3 import all_solutions


def permutation(variables, values):
    """返回 variables 是 values 的一个排列这一约束"""
    distinct_values = set(values)
    # 1. 每个元素都是 values 中含有的值之一
    exprs = [Or([x == v for v in distinct_values]) for x in variables]
    # 2. 每个值的出现次数与 values 相同
    exprs += [Sum([x == v for x in variables]) == values.count(v) for v in distinct_values]
    return And(exprs)


xs = IntVector('x', 4)
solver = Solver()
solver.add(permutation(xs, [1, 5, 5, 5]))

for m in all_solutions(solver):
    print([m[x] for x in xs])

[5, 5, 5, 1]
[1, 5, 5, 5]
[5, 5, 1, 5]
[5, 1, 5, 5]

[1, 5, 5, 5] 的排列共 \(4!/3! = 4\) 种，因此输出 4 行。重复的数越多，排列越少；若改用 Distinct()，这 4 种排列会减少到 0 种。

组装算式#

计算不按通常的优先级，而是按从左往右逐个运算的形式。之所以这样安排，是因为括号的位置本来就决定了运算顺序，把顺序固定成层序之后，全部括号写法就可以用“第几层合并哪两个”来描述。

s0 = n0 op0 n1
s1 = s0 op1 n2
s2 = s1 op2 n3      ← 算到 24 就成

这样只要四个数、三个运算符与三个中间结果，就能表示整个算式。

最后再由 s2 的值把原算式造出来，即还原成字符串的形式。

# 运算符编号 → 符号
# 0:+  1:-  2:*  3:/  4:反向的-  5:反向的/
OP_SYMBOLS = {0: '+', 1: '-', 2: '*', 3: '/', 4: '-', 5: '/'}


def output(numbers, ops):
    """从计算步骤（数的顺序和运算符序列）生成算式字符串"""
    def combine(n1, n2, op):
        if op in (4, 5):
            n1, n2 = n2, n1          # 反向的 - 和 / 交换左右再显示
        if isinstance(n1, str):
            n1 = f'({n1})'
        if isinstance(n2, str):
            n2 = f'({n2})'
        return f'{n1} {OP_SYMBOLS[op]} {n2}'

    expr = numbers[0]
    for n2, op in zip(numbers[1:], ops):
        expr = combine(expr, n2, op)
    return expr


print(output([1, 5, 5, 5], [3, 4, 2]))   # (5 - (1 / 5)) * 5
print(output([8, 3, 3, 8], [3, 4, 5]))   # 8 / (3 - (8 / 3))

(5 - (1 / 5)) * 5
8 / (3 - (8 / 3))

运算符的编号取到 0〜5，是为了把减法与除法左右对调的写法也各用一个编号表示。

  • - 需要 a - b 与 b - a 两种，这样不必增加数的排列也能两种都试到

  • / 同样需要 a / b 与 b / a 两种

只有减法与除法会因顺序不同而结果不同，因此把编号按左右两种写法分开，就不必再让数的排列去承担这部分工作。加与乘有交换律，a + b 与 b + a 同值，不必为此各留一个编号。

用 Z3 求解#

关键之处在于把四个数取为 Real，即实数，因为计算中途会出现 8 / 3 这样的分数，若取整数就无法表示。Z3 的整数除法会向下取整，8 / 3 得到的是 2，与实数运算的结果相差很远。

solve_24 在有解时返回算式的字符串，无解时返回 None。

def solve_24(*numbers):
    solver = Solver()
    n = RealVector('n', 4)      # 重排后的 4 个数（实数）
    op = IntVector('op', 3)     # 3 个运算符（0〜5）
    acc = RealVector('s', 3)    # 中途的计算结果

    solver.add(permutation(n, numbers))

    for x in op:
        solver.add(0 <= x, x < 6)

    def calc_op(n1, o, n2, res):
        """res == n1 (o) n2 这个约束"""
        return And(
            Implies(n2 == 0, o != 3),        # 不能除以 0
            Implies(n1 == 0, o != 5),
            Implies(o == 0, res == n1 + n2),
            Implies(o == 1, res == n1 - n2),
            Implies(o == 2, res == n1 * n2),
            Implies(o == 3, res == n1 / n2),
            Implies(o == 4, res == n2 - n1),  # 左右交换的减法
            Implies(o == 5, res == n2 / n1),  # 左右交换的除法
        )

    solver.add(calc_op(n[0], op[0], n[1], acc[0]))    # s0 = n0 op0 n1
    solver.add(calc_op(acc[0], op[1], n[2], acc[1]))  # s1 = s0 op1 n2
    solver.add(calc_op(acc[1], op[2], n[3], acc[2]))  # s2 = s1 op2 n3
    solver.add(acc[2] == 24)

    if solver.check() != sat:
        return None

    m = solver.model()
    numbers_used = [m.eval(x).as_long() for x in n]
    ops_used = [m.eval(x).as_long() for x in op]
    return output(numbers_used, ops_used)

下面解几道题，并用 eval() 确认造出的算式是否真的等于 24，也就是让 Python 再算一遍。这一步与 Z3 无关：eval() 走的是 Python 的算术，因此算式拼装时的笔误可以在这里暴露出来。

questions = [
    [1, 5, 5, 5],
    [3, 3, 8, 8],
    [3, 3, 7, 7],
    [1, 4, 5, 6],
    [2, 2, 2, 9],
    [2, 7, 8, 9],
    [6, 9, 9, 10],
    [1, 2, 7, 7],
    [4, 4, 10, 10],
    [2, 5, 5, 10],
]

for q in questions:
    expr = solve_24(*q)
    if expr is None:
        print(f'{q}: 无解')
    else:
        print(f'{q}: {expr} = {eval(expr):g}')

[1, 5, 5, 5]: (5 - (1 / 5)) * 5 = 24
[3, 3, 8, 8]: 8 / (3 - (8 / 3)) = 24
[3, 3, 7, 7]: ((3 / 7) + 3) * 7 = 24

[1, 4, 5, 6]: 6 / ((5 / 4) - 1) = 24

[2, 2, 2, 9]: ((2 + 9) * 2) + 2 = 24

[2, 7, 8, 9]: ((7 + 9) * 2) - 8 = 24
[6, 9, 9, 10]: (9 / (6 / 10)) + 9 = 24
[1, 2, 7, 7]: ((7 * 7) - 1) / 2 = 24
[4, 4, 10, 10]: ((10 * 10) - 4) / 4 = 24

[2, 5, 5, 10]: (5 - (2 / 10)) * 5 = 24

每道题都解出来了，不过 Z3 返回的是满足条件的第一个解，因此同一道题每次运行都可能得到不同的式子。要复现某个特定的式子，就得把它的形状作为约束写进去。例如 [1, 4, 5, 6] 可以写成下面两个式子，结果都是 24。

  • 6 / ((5 / 4) - 1)

  • 4 / (1 - (5 / 6))

用 Function 改写#

数的排列也可以用 Function() 表示成编号到数的对应表。

number_map = Function('number_map', IntSort(), RealSort())

这是接收整数、返回实数的函数，用 number_map(0) == numbers[0] 这样的写法把编号与数连接起来。

使用时给 indices = IntVector('i', 4) 加上 Distinct(indices) 的约束，使四个编号互不相同，而编号不同时从 number_map 取出的数自然就是一个排列。

def solve_24_by_function(*numbers):
    # 编号 → 数 的对应表
    number_map = Function('number_map', IntSort(), RealSort())

    solver = Solver()
    for i, v in enumerate(numbers):
        solver.add(number_map(i) == v)

    # 取出数的顺序（4 个编号互不相同）
    indices = IntVector('i', 4)
    for x in indices:
        solver.add(0 <= x, x < 4)
    solver.add(Distinct(indices))

    op = IntVector('op', 3)
    for x in op:
        solver.add(0 <= x, x < 6)

    acc = RealVector('s', 3)

    def calc_op(n1, o, n2, res):
        return And(
            Implies(n2 == 0, o != 3),
            Implies(n1 == 0, o != 5),
            Implies(o == 0, res == n1 + n2),
            Implies(o == 1, res == n1 - n2),
            Implies(o == 2, res == n1 * n2),
            Implies(o == 3, res == n1 / n2),
            Implies(o == 4, res == n2 - n1),
            Implies(o == 5, res == n2 / n1),
        )

    n = [number_map(i) for i in indices]
    solver.add(calc_op(n[0], op[0], n[1], acc[0]))
    solver.add(calc_op(acc[0], op[1], n[2], acc[1]))
    solver.add(calc_op(acc[1], op[2], n[3], acc[2]))
    solver.add(acc[2] == 24)

    if solver.check() != sat:
        return None

    m = solver.model()
    numbers_used = [m.eval(x).as_long() for x in n]
    ops_used = [m.eval(x).as_long() for x in op]
    return output(numbers_used, ops_used)


for q in questions:
    expr = solve_24_by_function(*q)
    print(f'{q}: {expr} = {eval(expr):g}')

[1, 5, 5, 5]: (5 - (1 / 5)) * 5 = 24
[3, 3, 8, 8]: 8 / (3 - (8 / 3)) = 24
[3, 3, 7, 7]: ((3 / 7) + 3) * 7 = 24

[1, 4, 5, 6]: 6 / ((5 / 4) - 1) = 24
[2, 2, 2, 9]: ((2 + 9) * 2) + 2 = 24

[2, 7, 8, 9]: ((7 + 9) * 2) - 8 = 24
[6, 9, 9, 10]: (10 / (6 / 9)) + 9 = 24

[1, 2, 7, 7]: ((7 * 7) - 1) / 2 = 24

[4, 4, 10, 10]: ((10 * 10) - 4) / 4 = 24
[2, 5, 5, 10]: (5 - (2 / 10)) * 5 = 24

得到的答案相同，两种方法只有排列的表示方式不同。

用 permutation()

用 Function

数的排列

用各值的出现次数约束

编号到数的对应表加 Distinct

有重复的数时

数出现次数，自然可以处理

编号不同即可取相同的值，同样自然

式子的长度

较短

稍长

两种写法都能解，而数的种类较多时，用对应表更好把握整体结构。代价是多一组 IntVector 与 Distinct，约束的数目比用出现次数时略多。

小结#

  • 四个数的排列，可以用 permutation() 按出现次数约束，也可以用 Function 加 Distinct 表示

  • 中间结果会出现分数，因此变量要取 Real

  • 运算符用 0〜5 的整数表示，再用 Implies 把该编号对应的计算逐个列出

  • 减法与除法把左右对调的写法也各留一个编号，就不必增加数的排列

  • 解不一定只有一个，Z3 返回的是满足条件的第一个解