演算子を入れて99を作る ― 括弧の付け方を Z3 に探させる

演算子を入れて99を作る ― 括弧の付け方を Z3 に探させる#

この章で学ぶこと#

数値の並びは決まっていて、間に +, -, * を入れて、括弧で計算の順序を変える問題です。

  • 「隣り合う2つを計算して1つに置き換える」を繰り返すと、どんな括弧の付け方も表せる

  • 各段階の配列を Z3 の変数にして、If で演算を選ぶ

  • 最後に、見つけた手順を数式の文字列に戻す

数の順序が自由な「24を作る」問題との違いも見えてきます。

次の式に対して、? に +, -, * のいずれかを入れ、括弧を適切に配置して式の値が 99 になるようにしてください。

1 ? 2 ? 3 ? 4 ? 5 ? 6 ? 7 ? 8 ? 9 = 99

考え方#

数を1つずつ計算していくのではなく、隣り合う2つを計算して1つにまとめる操作を繰り返します。

たとえば 1 2 3 4 5 から始めて、

  1. 3 + 4 を計算 → 1 2 7 5

  2. 1 * 2 を計算 → 2 7 5

  3. 7 + 5 を計算 → 2 12

  4. 2 - 12 を計算 → -10

のように、1段ごとに数が1つ減っていきます。最後に1つ残った数が式の値です。

        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」通りです。

1段ずつ計算する#

段階 l の配列を f[l] とします。最初の段階 f[0] は [1, 2, …, 9] で、段階が進むごとに1つ短くなります。

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]（1つ左からずれて残る）

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(条件, 真のときの値, 偽のときの値) を入れ子にして、3つの演算を切り替えています。

op

計算

0

x1 + x2

1

x1 - x2

2

x1 * x2

条件が増えると入れ子が深くなるので、選択肢が多いときは Function を使うほうが読みやすくなります（この章では3つなので If で十分です）。

数式として表示する#

Z3 が出すのは数だけなので、元の数式に戻す仕組みを用意します。Expr は「左の式、演算子、右の式」を持つ小さなクラスで、output() が段階の手順をたどって文字列を組み立てます。

* や - の右側に + や - が来るときは括弧を付けます。1 + 2 * 3 と (1 + 2) * 3 を取り違えないようにするためです。

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) です）。各段階の値も、1つずつ数が減っていく様子が分かります。

99になる組み合わせを探す#

こんどは位置と演算子を Z3 に決めさせます。9つの数なので、制約は「位置 locs[i] は 0 以上 9-i-1 未満」「演算子は 0〜2」です。

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 が見つけるのは条件を満たす最初の1つなので、式の形は毎回同じとは限りません。どれも 99 になります。

まとめ#

  • 固定された数の並びに対する括弧の付け方は、「隣り合う2つをまとめる」操作の列で表せる

  • 段階ごとに配列を用意し、calc_tree() で「残る・計算する・ずれる」の3通りを Implies で書く

  • 演算子は整数の番号にして、If で計算を切り替える

  • 見つけた手順は、計算の木（Expr）に戻せば数式として読める

  • 数の順序も自由な「24を作る」問題では、順列の制約がもう1つ増える（前の章）