24を作る ― 4つの数と演算子の組み合わせを探す

24を作る ― 4つの数と演算子の組み合わせを探す#

この章で学ぶこと#

「24を作る」パズルを Z3 で解きます。4つの数と3つの演算子、それに計算の順序を決めれば答えが出ます。

  • 4つの数は「順列」なので、並べ替えを制約で表す（重複した数があっても動く）

  • 途中結果が分数になるので、変数は Real（実数）にする

  • 演算子は 0〜5 の整数で表し、Implies で「その番号のときの計算」を書く

同じ問題を、Function() を使って書き直すバージョンも作ります。

問題#

4つの数 +, -, *, / と括弧を使って、答えが 24 になる式を作ってください。

たとえば [1, 5, 5, 5] なら

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

が答えの1つです。数を並べ替える方法は \(4! = 24\) 通り（同じ数があればその分だけ減ります）、演算子の選び方は \(6^3\) 通り（後述）です。人が手で探すと大変なので、Z3 に探させます。

数の順列を制約で表す#

solve_24 では、4つの数を「並べ替えたもの」として持ちたいので、順列の制約を作ります。

permutation(xs, values) は、xs が values の並べ替えになるように制約を返します。

  1. xs の各要素は、values に含まれる値のどれか

  2. 値 v ごとに、xs の中に現れる回数が values の中の回数と同じ

[1, 5, 5, 5] なら「1 が1回、5 が3回」です。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つだけ出力されます。

数式を組み立てる#

計算は「左から順に1つずつ演算する」形にします。

s0 = n0 op0 n1
s1 = s0 op1 n2
s2 = s1 op2 n3      ← これが 24 になればよい

この形にすると、4つの数と3つの演算子、3つの中間結果だけで式を表せます。

最後に、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 まであるのは、引き算と割り算の左右を入れ替えた形も1つの番号で表すためです。

  • - は a - b と b - a の両方が必要（数を並べ替えずに両方試せる）

  • / も同様に a / b と b / a が必要

引き算・割り算だけは順序で答えが変わるので、番号を分けておくと、数の並べ替えを無駄に増やさずに済みます。

Z3 で解く#

4つの数を Real（実数）にしているのがポイントです。途中で 8 / 3 のような分数が出てくるので、整数にすると計算が合いません。

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 になるかを確かめています。

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つを返すので、同じ問題でも実行するたびに別の式になることがあります。たとえば [1, 4, 5, 6] は

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

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

のどちらでも 24 になります。

Function で書き直す#

数の順列は、Function() を使って「番号 → 数の対応表」としても表せます。

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

これは「整数を受け取って実数を返す関数」です。number_map(0) == numbers[0] のように、番号と数を結びつけます。

使うときは、indices = IntVector('i', 4) に Distinct(indices) を課して、4つの番号がすべて違うようにします。番号が違えば 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

同じ答えが出ました。2つの方法の違いは「順列の表し方」だけです。

permutation() を使う

Function を使う

数の並べ替え

値の出現回数で制約

番号 → 数 の対応表 + Distinct

同じ数が複数あるとき

出現回数を数えるので自然に扱える

番号が違えば同じ値でもよい（自然に扱える）

式の長さ

短い

少し長い

どちらでも解けます。数の種類が多い問題なら、対応表のほうが見通しがよくなります。

まとめ#

  • 4つの数の並べ替えは、permutation()（出現回数で縛る）か Function + Distinct で表せる

  • 途中結果が分数になるので、変数は Real にする

  • 演算子は 0〜5 の整数で表し、Implies で「その番号のときの計算」を並べる

  • 引き算・割り算は左右を入れ替えた形も番号で用意すると、数の並べ替えを増やさずに済む

  • 解は1つとは限らない。Z3 は条件を満たす最初の1つを返す