2021 d24: add input and original solution

Author: mebeim

2021/inputs/2021_24.txt

@@ -0,0 +1,252 @@
+inp w
+mul x 0
+add x z
+mod x 26
+div z 1
+add x 12
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 4
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 1
+add x 15
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 11
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 1
+add x 11
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 7
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 26
+add x -14
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 2
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 1
+add x 12
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 11
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 26
+add x -10
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 13
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 1
+add x 11
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 9
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 1
+add x 13
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 12
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 26
+add x -7
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 6
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 1
+add x 10
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 2
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 26
+add x -2
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 11
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 26
+add x -1
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 12
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 26
+add x -4
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 3
+mul y x
+add z y
+inp w
+mul x 0
+add x z
+mod x 26
+div z 26
+add x -12
+eql x w
+eql x 0
+mul y 0
+add y 25
+mul y x
+add y 1
+mul z y
+mul y 0
+add y w
+add y 13
+mul y x
+add z y

2021/original_solutions/day24.py

@@ -0,0 +1,49 @@
+import z3
+
+def add_constraints(s, inp):
+	for digit in inp:
+		s.add(digit > 0)
+		s.add(digit < 10)
+
+	v5 = inp[1]
+	v6 = (inp[0] + 4) * (inp[0] != 12) % 26 + 15 != v5
+	v7 = (v5 + 11) * v6 + (25 * v6 + 1) * (inp[0] + 4) * (inp[0] != 12)
+	v8 = (inp[2] + 7) * (v7 % 26 + 11 != inp[2]) + (25 * (v7 % 26 + 11 != inp[2]) + 1) * v7
+	v9 = (inp[3] + 2) * (v8 % 26 - 14 != inp[3]) + v8 / 26 * (25 * (v8 % 26 - 14 != inp[3]) + 1)
+	v10 = (inp[4] + 11) * (v9 % 26 + 12 != inp[4]) + v9 * (25 * (v9 % 26 + 12 != inp[4]) + 1)
+	v11 = (inp[5] + 13) * (v10 % 26 - 10 != inp[5]) + v10 / 26 * (25 * (v10 % 26 - 10 != inp[5]) + 1)
+	v12 = (inp[6] + 9) * (v11 % 26 + 11 != inp[6]) + (25 * (v11 % 26 + 11 != inp[6]) + 1) * v11
+	v13 = (inp[7] + 12) * (v12 % 26 + 13 != inp[7]) + (25 * (v12 % 26 + 13 != inp[7]) + 1) * v12
+	v14 = (inp[8] + 6) * (v13 % 26 - 7 != inp[8]) + v13 / 26 * (25 * (v13 % 26 - 7 != inp[8]) + 1)
+	v15 = (inp[9] + 2) * (v14 % 26 + 10 != inp[9]) + v14 * (25 * (v14 % 26 + 10 != inp[9]) + 1)
+	v16 = (inp[10] + 11) * (v15 % 26 - 2 != inp[10]) + v15 / 26 * (25 * (v15 % 26 - 2 != inp[10]) + 1)
+	v17 = (inp[11] + 12) * (v16 % 26 - 1 != inp[11]) + v16 / 26 * (25 * (v16 % 26 - 1 != inp[11]) + 1)
+	v18 = (inp[12] + 3) * (v17 % 26 - 4 != inp[12]) + v17 / 26 * (25 * (v17 % 26 - 4 != inp[12]) + 1)
+	res = (inp[13] + 13) * (v18 % 26 - 12 != inp[13]) + v18 / 26 * (25 * (v18 % 26 - 12 != inp[13]) + 1)
+
+	tot = 0
+	for digit in inp:
+		tot = tot * 10 + digit
+
+	s.add(res == 0)
+	return tot
+
+def solve(inp, maximize=True):
+	s = z3.Optimize()
+	value = add_constraints(s, inp)
+
+	if maximize:
+		s.maximize(value)
+	else:
+		s.minimize(value)
+
+	assert s.check() == z3.sat
+
+	m = s.model()
+	return m.eval(value)
+
+
+inp = [z3.Int('x{}'.format(i)) for i in range(14)]
+
+print('Part 1:', solve(inp, maximize=True))
+print('Part 2:', solve(inp, maximize=False))