Using a SAT solver to do Day 24 of Advent of Code
I’ve been doing Advent of Code this year with coworkers (did it later year too) and day 24 was actually funny enough to write about.
So on Day 24 of Advent of Code they gave us this problem where it’s basically: write a program that takes in a program as assembly and runs it against a 14 digit number (with no zeros) and finds the answer where z=0.
The assembly is pretty straight forward, there’s just ops for multiplying, adding, dividing, modulo, equality and taking in input that set x,z,y,w registers.
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 7
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
...
You can try to write a bruteforcer that does this (like I did) but it’s pretty impractical since the input w is a 14 digit number and that’s too big for all the possible values.
So what I found out (perusing reddit lol) was you can just parse the input, convert it into C code and then compile it with as many compiler flags as possible (I guess) and then put it into Ghidra, get the simplified source code and then put it into z3. You could probably skip the “put it into Ghidra step” but I did this anyway.
import z3
def to_val(inp):
res = 0
for d in inp:
res = res*10 + d
return res
def add_constraints(s, inp):
for digit in inp:
s.add(digit > 0)
s.add(digit < 10)
uVar1 = (inp[0] + 7) * (inp[0] != 12)
uVar2 = (uVar1 % 26 + 13 != inp[1])
uVar1 = uVar1 * (uVar2 * 25 + 1) + (inp[1] + 8) * uVar2
uVar2 = (uVar1 % 26 + 13 != inp[2])
uVar1 = uVar1 * (uVar2 * 25 + 1) + (inp[2] + 10) * uVar2
uVar2 = (uVar1 % 26 - 2 != inp[3])
uVar1 = (uVar1 / 0x1a) * (uVar2 * 0x19 + 1) + (inp[3] + 4) * uVar2
uVar2 = (uVar1 % 26 - 10 != inp[4])
uVar1 = (uVar1 / 0x1a) * (uVar2 * 0x19 + 1) + (inp[4] + 4) * uVar2
uVar2 = (uVar1 % 26 + 13 != inp[5])
uVar1 = uVar1 * (uVar2 * 25 + 1) + (inp[5] + 6) * uVar2
uVar2 = (uVar1 % 26 - 14 != inp[6])
uVar1 = (uVar1 / 0x1a) * (uVar2 * 0x19 + 1) + (inp[6] + 0xb) * uVar2
uVar2 = (uVar1 % 26 - 5 != inp[7])
uVar1 = (uVar1 / 0x1a) * (uVar2 * 25 + 1) + (inp[7] + 0xd) * uVar2
uVar2 = (uVar1 % 26 + 15 != inp[8])
uVar1 = uVar1 * (uVar2 * 25 + 1) + (inp[8] + 1) * uVar2
uVar2 = (uVar1 % 26 + 15 != inp[9])
uVar1 = uVar1 * (uVar2 * 25 + 1) + (inp[9] + 8) * uVar2;
uVar2 = (uVar1 % 26 - 14 != inp[10])
uVar1 = (uVar1 / 26) * (uVar2 * 25 + 1) + (inp[10] + 4) * uVar2
uVar2 = (uVar1 % 26 + 10 != inp[11])
uVar1 = uVar1 * (uVar2 * 25 + 1) + (inp[11] + 0xd) * uVar2
uVar2 = (uVar1 % 26 - 14 != inp[12])
uVar1 = (uVar1 / 26) * (uVar2 * 25 + 1) + (inp[12] + 4) * uVar2
uVar2 = (uVar1 % 26 - 5 != inp[13]);
res = (uVar1 / 0x1a) * (uVar2 * 25 + 1) + (inp[13] + 14) * uVar2
s.add(res == 0)
return to_val(inp)
def solve(inp):
s = z3.Optimize()
value = add_constraints(s, inp)
s.maximize(value) # maximize, you can change this for part 2
assert s.check() == z3.sat
m = s.model()
return m.eval(value)
inp = [z3.Int('x{}'.format(i)) for i in range(14)]
print(solve(inp))
def prog_to_python(prog):
s = ""
for p in prog:
instr, ops = p
if instr == "add":
s += ops[0] + "+=" + str(ops[1]) + ";"
elif instr == "mod":
s += ops[0] + "%=" + str(ops[1]) + ";"
elif instr == "div":
s += ops[0] + "/=" + str(ops[1]) + ";"
elif instr == "mul":
s += ops[0] + "*=" + str(ops[1]) + ";"
elif instr == "eql":
s += ops[0] + "=" + ops[0] + "==" + str(ops[1]) + "?1:0;"
elif instr == "inp":
s += "w=bla;"
else:
print(instr,ops)
assert(False)
s += "\n"
print(s)
prog = []
for line in lines:
sp = line.split(" ")
instr = sp[0]
ops = sp[1:]
if len(ops) > 1 and ops[1] not in ["x","y","z","w"]:
ops[1] = int(ops[1])
prog.append((instr,ops))
Note that the above SAT code is taken from my input which I took from Ghidra to form the z3 eqns
uVar1 = (param_1 + 7) * (uint)(param_1 != 12);
uVar2 = (uint)(uVar1 % 26 + 13 != param_2);
uVar1 = uVar1 * (uVar2 * 25 + 1) + (param_2 + 8) * uVar2;
uVar2 = (uint)(uVar1 % 26 + 13 != param_3);
uVar1 = uVar1 * (uVar2 * 25 + 1) + (param_3 + 10) * uVar2;
uVar2 = (uint)(uVar1 % 26 - 2 != param_4);
uVar1 = (uVar1 / 0x1a) * (uVar2 * 0x19 + 1) + (param_4 + 4) * uVar2;
uVar2 = (uint)(uVar1 % 26 - 10 != param_5);
uVar1 = (uVar1 / 0x1a) * (uVar2 * 0x19 + 1) + (param_5 + 4) * uVar2;
uVar2 = (uint)(uVar1 % 26 + 13 != param_6);
uVar1 = uVar1 * (uVar2 * 25 + 1) + (param_6 + 6) * uVar2;
uVar2 = (uint)(uVar1 % 26 - 14 != param_7);
uVar1 = (uVar1 / 0x1a) * (uVar2 * 0x19 + 1) + (param_7 + 0xb) * uVar2;
uVar2 = (uint)(uVar1 % 26 - 5 != param_8);
uVar1 = (uVar1 / 0x1a) * (uVar2 * 25 + 1) + (param_8 + 0xd) * uVar2;
uVar2 = (uint)(uVar1 % 26 + 15 != param_9);
uVar1 = uVar1 * (uVar2 * 25 + 1) + (param_9 + 1) * uVar2;
uVar2 = (uint)(uVar1 % 26 + 15 != param_10);
uVar1 = uVar1 * (uVar2 * 25 + 1) + (param_10 + 8) * uVar2;
uVar2 = (uint)(uVar1 % 26 - 14 != param_11);
uVar1 = (uVar1 / 26) * (uVar2 * 25 + 1) + (param_11 + 4) * uVar2;
uVar2 = (uint)(uVar1 % 26 + 10 != param_12);
uVar1 = uVar1 * (uVar2 * 25 + 1) + (param_12 + 0xd) * uVar2;
uVar2 = (uint)(uVar1 % 26 - 14 != param_13);
uVar1 = (uVar1 / 26) * (uVar2 * 25 + 1) + (param_13 + 4) * uVar2;
uVar2 = (uint)(uVar1 % 26 - 5 != param_14);
return (uVar1 / 0x1a) * (uVar2 * 25 + 1) + (param_14 + 14) * uVar2; // z value
And that’s about it. I got 79197919993985 for part 1 and 13191913571211 for part 2, best of all the solver can do this within 20-30 seconds on a 2019 mbp.
Conclusion
I think this was a really clever way of solving this problem that is totally reasonable since you may not want to reverse engineer all of that C code into figuring out what the max/min value you can give the input is. Definitely keep knowledge of z3/SAT in your arsenal. Plus, this is in theory a solution that could be done SUPER quickly if you were fast enough.
Back