Almost recreational math: missing operation(s) puzzle

The equation:
1 ? 2 ? 3 ? 4 ? 5 ? 6 ? 7 ? 8 ? 9 = 0

Fill ? with -, + or * operation, and find such a sequence, so that the equation would be true. This is tricky, because of operator precedence, multiplication must be handled at first. Brackets are also possible.

See also: https://www.dcode.fr/missing-operators-equation-solver, https://brilliant.org/wiki/arithmetic-puzzles-operator-search/.

To solve this, I just enumerate all possible ordered binary search tree of 9 elements, which are almost the same as expression with 9 terms and all possible variations of brackets.

Then we try each expression...

from z3 import *

CONST=1234
TOTAL=9

# prepare a list in form: [(1,"1"),(2,"2"),(3,"3")...]
# rationale: enum_ordered() yields both expression tree and expression as a string...
input_values=[]
for i in range(TOTAL):
    input_values.append((i+1, str(i+1)))

OPS=TOTAL-1

ops=[Int('op_%d' % i) for i in range(OPS)]

# this is a hack... operation number. resetting after each tree:
n=-1

# select operation...
def op(l, r, n):
    return If(ops[n]==0, l+r,
        If(ops[n]==1, l-r,
        If(ops[n]==2, l*r,
        0))) # default

# enumerate all possible ordered binary search trees
# copypasted from https://stackoverflow.com/questions/14900693/enumerate-all-full-labeled-binary-tree
# this generator yields both expression and string

# expression may have form like (please note, many constants are optimized/folded):

# If(op_1 == 0,
#    1 +
#    If(op_0 == 0, 5, If(op_0 == 1, -1, If(op_0 == 2, 6, 0))),
#    If(op_1 == 1,
#       1 -
#       If(op_0 == 0,
#          5,
#          If(op_0 == 1, -1, If(op_0 == 2, 6, 0))),
#       If(op_1 == 2,
#          1*
#          If(op_0 == 0,
#             5,
#             If(op_0 == 1, -1, If(op_0 == 2, 6, 0))),
#          0)))

# string is like "(1 op1 (2 op0 3))", opX substring will be replaced by operation name after (-, +, *)

def enum_ordered(labels):
    global n
    if len(labels) == 1:
        yield (labels[0][0], labels[0][1])
    else:
        for i in range(1, len(labels)):
            for left in enum_ordered(labels[:i]):
                for right in enum_ordered(labels[i:]):
                    n=n+1
                    yield (op(left[0], right[0], n), "("+left[1]+" op"+str(n)+" "+right[1]+")")

for tree in enum_ordered(input_values):
    s=Solver()
    # operations in 0..2 range...
    for i in range(OPS):
        s.add(And(ops[i]>=0, ops[i]<=2))
    s.add(tree[0]==CONST)
    if s.check()==sat:
        m=s.model()
        tmp=tree[1]
        for i in range(OPS):
            op_s=["+", "-", "*"][m[ops[i]].as_long()]
            tmp=tmp.replace("op"+str(i), op_s)
        print tmp, "=", eval(tmp)
    n=-1


For 9 terms, there are 1430 binary trees, or expressions (9th Catalan number).

For 0, there are 1391 solutions, some of them:

(1 + (2 + (3 + (4 + (5 * (6 - (7 - (8 - 9)))))))) = 0                                                     
(1 + (2 + (3 + (4 + (5 * (6 - ((7 - 8) + 9))))))) = 0
(1 + (2 + (3 + (4 + (5 * ((6 - 7) + (8 - 9))))))) = 0
(1 + (2 + (3 - (4 + (5 - ((6 * (7 - 8)) + 9)))))) = 0
(1 + (2 + (3 + (4 + (5 * (((6 - 7) + 8) - 9)))))) = 0
(1 - (2 + (3 + (4 + ((5 - 6) + (7 * (8 - 9))))))) = 0
(1 - (2 + (3 + (4 + ((5 - 6) * ((7 - 8) + 9)))))) = 0

...

((((((1 - (2 - 3)) * (4 - 5)) - 6) + 7) - 8) + 9) = 0
(((((((1 - 2) + 3) + (4 - 5)) * 6) - 7) - 8) + 9) = 0
((((((1 + (2 * (3 * 4))) + 5) - 6) - 7) - 8) - 9) = 0
((((((1 * ((2 + 3) + 4)) - 5) + 6) + 7) - 8) - 9) = 0
(((((((1 + 2) - (3 + 4)) + 5) + 6) - 7) * 8) * 9) = 0
(((((((1 * (2 - 3)) * 4) + 5) * 6) - 7) - 8) + 9) = 0
((((((((1 - 2) + 3) + 4) * 5) - 6) - 7) - 8) - 9) = 0  

There are no solutions for 5432. But for 5430:

(1 + (2 + (3 * ((4 * (5 * (6 * (7 + 8)))) + 9)))) = 5430                                                  
(1 + (2 + (3 * ((4 * ((5 * 6) * (7 + 8))) + 9)))) = 5430
(1 + (2 + (3 * (((4 * 5) * (6 * (7 + 8))) + 9)))) = 5430
(1 + (2 + (3 * (((4 * (5 * 6)) * (7 + 8)) + 9)))) = 5430
(1 + (2 + (3 * ((((4 * 5) * 6) * (7 + 8)) + 9)))) = 5430
((1 + 2) + (3 * ((4 * (5 * (6 * (7 + 8)))) + 9))) = 5430

Surely, several of these expressions are equivalent to each other, due to associative property of multiplication and addition.

For 1234:

(1 * (2 * (((3 - (4 - ((5 + 6) * 7))) * 8) + 9))) = 1234                                                  
(1 + (2 + ((((3 * ((4 + 5) * 6)) - 7) * 8) - 9))) = 1234
(1 + (2 + (((((3 * (4 + 5)) * 6) - 7) * 8) - 9))) = 1234
(1 + ((2 + (3 * ((4 + 5) * (6 + (7 - 8))))) * 9)) = 1234
(1 + ((2 + (3 * ((4 + 5) * ((6 + 7) - 8)))) * 9)) = 1234
(1 + ((2 + (3 * ((4 + (5 - 6)) * (7 + 8)))) * 9)) = 1234
(1 + ((2 + (3 * (((4 + 5) - 6) * (7 + 8)))) * 9)) = 1234
(1 + ((2 + (3 * (((4 * (5 + 6)) - 7) + 8))) * 9)) = 1234
(1 + ((2 + ((3 * (4 + 5)) * (6 + (7 - 8)))) * 9)) = 1234
(1 - ((2 - (((3 + 4) * 5) + ((6 + 7) * 8))) * 9)) = 1234
(1 + ((2 + ((3 * (4 + (5 - 6))) * (7 + 8))) * 9)) = 1234
(1 + ((2 + ((3 * ((4 + 5) - 6)) * (7 + 8))) * 9)) = 1234
(1 + ((2 - (((3 * (4 - 5)) - 6) * (7 + 8))) * 9)) = 1234
(1 - ((2 + ((3 * ((4 - (5 + 6)) * 7)) + 8)) * 9)) = 1234
(1 - ((2 + ((3 * (((4 - 5) - 6) * 7)) + 8)) * 9)) = 1234
(1 - ((2 + (((3 * (4 - (5 + 6))) * 7) + 8)) * 9)) = 1234
(1 - ((2 + (((3 * ((4 - 5) - 6)) * 7) + 8)) * 9)) = 1234
(1 - ((2 - ((((3 * (4 + 5)) - 6) * 7) - 8)) * 9)) = 1234
(1 - (((2 - ((3 + 4) * 5)) - ((6 + 7) * 8)) * 9)) = 1234
(1 - (((2 - ((3 + (4 * 5)) * 6)) + (7 - 8)) * 9)) = 1234
(1 + (((2 + (3 - (4 * (5 - (6 * 7))))) * 8) + 9)) = 1234
(1 + (((2 + (3 + (4 * ((5 * 6) + 7)))) * 8) + 9)) = 1234
(1 - (((2 + (3 * ((4 - (5 + 6)) * 7))) + 8) * 9)) = 1234
(1 - (((2 + (3 * (((4 - 5) - 6) * 7))) + 8) * 9)) = 1234
(1 - (((2 + ((3 * (4 - (5 + 6))) * 7)) + 8) * 9)) = 1234
(1 - (((2 + ((3 * ((4 - 5) - 6)) * 7)) + 8) * 9)) = 1234
(1 - (((2 - (((3 + (4 * 5)) * 6) - 7)) - 8) * 9)) = 1234
(1 + ((((2 + 3) - (4 * (5 - (6 * 7)))) * 8) + 9)) = 1234
(1 - ((((2 - (3 * ((4 + 5) * 6))) + 7) * 8) - 9)) = 1234
(1 - ((((2 - ((3 + (4 * 5)) * 6)) + 7) - 8) * 9)) = 1234
((1 + 2) + ((((3 * ((4 + 5) * 6)) - 7) * 8) - 9)) = 1234
((1 + 2) + (((((3 * (4 + 5)) * 6) - 7) * 8) - 9)) = 1234
((1 + (2 + (((3 * ((4 + 5) * 6)) - 7) * 8))) - 9) = 1234
((1 + (2 + ((((3 * (4 + 5)) * 6) - 7) * 8))) - 9) = 1234
((1 + ((2 + (3 - (4 * (5 - (6 * 7))))) * 8)) + 9) = 1234
((1 + ((2 + (3 + (4 * ((5 * 6) + 7)))) * 8)) + 9) = 1234
((1 - ((2 - ((3 * ((4 + 5) * 6)) - 7)) * 8)) + 9) = 1234
((1 - ((2 - (((3 * (4 + 5)) * 6) - 7)) * 8)) + 9) = 1234
((1 + (((2 + 3) - (4 * (5 - (6 * 7)))) * 8)) + 9) = 1234
((1 - (((2 - (3 * ((4 + 5) * 6))) + 7) * 8)) + 9) = 1234
((1 - (((2 - ((3 * (4 + 5)) * 6)) + 7) * 8)) + 9) = 1234
(((1 + 2) + (((3 * ((4 + 5) * 6)) - 7) * 8)) - 9) = 1234
(((1 + 2) + ((((3 * (4 + 5)) * 6) - 7) * 8)) - 9) = 1234

The problem is easy enough to be solved using my toy-level MK85 SMT-solver:

from MK85 import *

n=-1

CONST=13

#TOTAL=9
TOTAL=7

BIT_WIDTH=8

s=MK85(verbose=0)

input_values=[]
for i in range(TOTAL):
    input_values.append((s.BitVecConst(i+1, BIT_WIDTH), str(i+1)))

OPS=TOTAL-1

ops=[s.BitVec('op_%d' % i,2) for i in range(OPS)]

for i in range(OPS):
    s.add(And(ops[i]>=0, ops[i]<=2))

def op(l, r, n):
    return s.If(ops[n]==s.BitVecConst(0, 2), l+r,
        s.If(ops[n]==s.BitVecConst(1, 2), l-r,
        s.If(ops[n]==s.BitVecConst(2, 2), l*r,
            s.BitVecConst(0, BIT_WIDTH))))

def enum_ordered(labels):
    global n
    if len(labels) == 1:
        yield (labels[0][0], labels[0][1])
    else:
        for i in range(1, len(labels)):
            for left in enum_ordered(labels[:i]):
                for right in enum_ordered(labels[i:]):
                    n=n+1
                    yield (op(left[0], right[0], n), "("+left[1]+" op"+str(n)+" "+right[1]+")")

for tree in enum_ordered(input_values):
    s.add(tree[0]==CONST)

    for i in range(OPS):
        s.add(ops[i]!=3)

    if s.check():
        m=s.model()
        #print "sat", tree[1]
        tmp=tree[1]
        for i in range(OPS):
            op_s=["+", "-", "*"][m['op_%d' % i]]
            tmp=tmp.replace("op"+str(i), op_s)
        print tmp, "=", eval(tmp)
        # show only first solution...
        exit(0)



→ [list of blog posts]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.