# 4x4 grid equations

Can you place all numbers from 1 to 16 into cells, such that the following 8 equations hold? Note that the operator "/" only works for non-remainder division, i.e. you can have "8 / 4" but not "8 / 3". As usual multiplication and division are performed before addition and subtraction. Good luck! • I would say no computers, although it is still hard with a computer as you need to check 15! combinations. Oct 7, 2020 at 2:35
• Don't underestimate SMT solvers. With properly coded constraints, Z3 can solve this in under a second! Oct 7, 2020 at 3:56

$$\begin{array}{ccccccc}9 & + & 16 & \div & 8 & = & 11 \\+&&-&&-&&+\\6 & \div & 3 & + & 12 & = & 14 \\\times&&\times&&\div&&\div\\1 & + & 2 & + & 4 & = & 7 \\=&&=&&=&&=\\15 & - & 10 & \div & 5 & = & 13\end{array}$$

(Partial) Explanation:

Let's label the grid as follows:

$$\begin{array}{ccccccc}A & + & B & \div & C & = & D \\+&&-&&-&&+\\E & \div & F & + & G & = & H \\\times&&\times&&\div&&\div\\I & + & J & + & K & = & L \\=&&=&&=&&=\\M & - & N & \div & O & = & P\end{array}$$

Observe that there are five divisions, none of which share any number. Since all numbers are distinct, the ratios must be at least 2, and therefore the divisors cannot exceed 8. The positions for divisors are $$C, F, K, L, O$$. Also since $$I+J+K=L$$, it follows that all of $$I,J,K$$ are less than $$L$$, and therefore they cannot exceed 8 either. So far, we've identified seven cells that cannot exceed 8: $$C, F, I, J, K, L, O$$. Also, if you're familiar with Kakuro, you can notice that 1 must be one of $$I,J,K$$ from $$I+J+K=L \le 8$$.

Now consider the two prime numbers 11 and 13. They cannot be a part of division (neither dividend nor divisor): They cannot divide anything else and they cannot be divided by anything else other than 1. The only place where 1 can divide something is $$G \div K$$, but then $$C$$ becomes too high. Therefore, 11 and 13 must be placed in $$ADPM$$.

Also note that $$A \rightarrow D \rightarrow P \rightarrow M$$ forms a strictly increasing sequence with gaps of at least 2, since the quotients are at least 2 and

\begin{align}A + B \div C &= D \\D + H \div L &= P \\P + N \div O &= M\end{align}

So 11 and 13 must be adjacent in the sequence. If they're assigned to $$AD$$, $$M$$ gets too large, so the only options are $$D=11, P=13$$ or $$P=11, M=13$$.

At this point, combined with the information that $$HL$$ can only be one of $$(12,6),(14,7),(16,8)$$, I started brute-forcing the cells, and I was lucky that I guessed the 3rd row and 4th column correctly early on.

As a bonus, a computer-based proof that the solution is unique (Python + Z3Py):

import z3

solver = z3.SolverFor('QF_FD')
varlist = [z3.Int(var) for var in 'abcdefghijklmnop']
for var in varlist:
solver += 0 < var
solver += var <= 16
solver += z3.Distinct(varlist)

a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p = varlist

solver += b == c * (d - a)
solver += e == f * (h - g)
solver += l == i + (j + k)
solver += n == o * (m - p)
solver += m == a + (e * i)
solver += n == b - (f * j)
solver += g == k * (c - o)
solver += h == l * (p - d)
assert solver.check() != z3.unsat
model = solver.model()
for var in varlist:
print(model.eval(var), end=' ')
print()
solver += z3.Or(*[var != model.eval(var) for var in varlist])
assert solver.check() == z3.unsat
print('No more solutions')

Output:

9 16 8 11 6 3 12 14 1 2 4 7 15 10 5 13
No more solutions

• Wow that is amazing! I didn't think anyone would get it so quickly. I am truly impressed. Well done! Oct 7, 2020 at 2:40
• Very nice explanation too. Oct 7, 2020 at 3:50
• love the z3 code - makes it look easy. Oct 7, 2020 at 12:45