Introduction

Advent of Code is an annual set of programming puzzles, released day by day in December (like an advent calendar).

On Day 21, we're given a tiny reprogrammable robot and asked to write a program so that it can walk across the hull of a ship, jumping over any missing gaps.

It looks something like this:

The program is up to 15 instructions in SpringScript, a fictional programming language. Each instruction contains an opcode (AND, OR, or NOT), a source register, and a target register.

The robot has two writeable target registers: T (the temporary register) and J (the jump register). At the end of program execution, if J is True, then the robot jumps four tiles ahead.

In addition, the robot provides sensor data in read-only registers A through I. These registers mark whether upcoming tiles are filled (True) or empty (False).

A naive solution jumps if the upcoming tile is empty.

Test it out in the simulation below:

This isn't going to work in all cases, and will fail for the map below.

Can you write a script to solve this map? Edit the textbox on the left, or press "Load solution" to see an answer.

Solving manually

Based on the Reddit Solutions Thread, many people took a similar approach:

I started with a similar approach, building up a map that collects the "danger zones" where the robot has fallen. It looks something like this:

(As before, you can write a script and try to solve this map – it's not too hard!)

This is a relatively manual process, though some folks automated it with genetic algorithms and other search strategies.

What would a robust, automatic, general-purpose solver look like?

Phrasing our problem

Let's start from our goal:

If I were a jumping robot, I would simply make sure to be in the air whenever there's a pit below me.

Because a jump always covers four tiles, a robot is in the air if it has jumped within the last three tiles. At any given tile, a robot jumps if it is not already in the air, and its script tells it to jump given the sensor readings.

We want to find a program for which the goal above is true, given a particular map.

Enter Z3

Each instruction can be recorded as a 7-bit value:

The entire program is therefore 7 * 15 = 105 bits of data, so there are roughly 40564819207303340847894502572031 possible programs.

This would take a little while to search by hand. Luckily, we have a large hammer available: we'll be using Z3, an automated theorem prover from Microsoft Research.

Our plan is to symbolically execute the program defined by our 105 bits, without fixing them to any particular value. Then, we'll be able to make statements about when the robot must jump, and ask the solver to find a program that meets those conditions.

Here's the code to do this symbolic evaluation:

def symbolic_execution(length=15):
    ''' Symbolically executes a program of a given length

        Returns (f, prog):
        - f is a lambda function which should be called with a map
         of sensor readings, and returns the symbolic result
        - prog is a list of (opcode, reg_in, reg_out) tuples
    '''
    # Initialize the T and J registers to False
    T = BoolVal(False)
    J = BoolVal(False)
    sensors = {c:Bool(c) for c in 'ABCDEFGHI'}
    program = []

    for i in range(length):
        op = BitVec('op_%i' % i, 2)
        reg_in = BitVec('reg_in_%i' % i, 4)
        reg_out = BitVec('reg_out_%i' % i, 1)

        # Pick out our left-hand argument based on reg_in
        lhs = T # default value
        for (i, r) in enumerate(list(sensors.values()) + [T, J]):
            lhs = If(reg_in == i, r, lhs)

        # Pick out our right-hand argument based on reg_in
        # This is ignored if the opcode is NOT, but we can't know
        # that going in, since we're executing symbolically.
        rhs = If(reg_out == 0, T, J)

        # Calculate the result based on opcode
        result = If(op == 0, And(lhs, rhs),
                 If(op == 1, Or(lhs, rhs),
                             Not(lhs)))

        # Write the result to either T or J; the other one
        # keeps the value from the previous iteration.
        (T, J) = (If(reg_out == 0, result, T),
                  If(reg_out == 1, result, J))

        program.append([op, reg_in, reg_out])

    # Helper function to bind sensor readings
    f = lambda vs: substitute(J,
        *[(v, BoolVal(vs[k]) if type(vs[k]) is bool else vs[k])
          for (k, v) in sensors.items()])

    return (f, program)

Each instruction is a tuple [opcode, input_reg, output_reg], which are each a BitVec value (i.e. integers of a fixed bit length, whose values are unknown until the solver picks them).

When executing, we track the temporary and jump registers T and J, updating them at each instruction based on whether they're the output of that instruction. The final value for J represents whether to jump at the end of of the program.

This value is generic in terms of the program, but also in terms of sensor readings, which isn't quite what we want – we'd like to make assertions given a fixed set of sensor readings, rather than letting the solver pick them.

To fix this, we wrap J in a lambda function which applies a particular set of sensor readings; think of this as partial evaluation with respect to the sensor registers.

We can immediately use this to do interesting things. Let's solve for a one-instruction program which jumps if the A sensor register is False.

>>> (f, prog) = symbolic_execution(1)
>>> solver = Solver()
>>> sensors = {'A': False, **{c: True for c in 'BCDEFGHI'}}
>>> solver.add(f(sensors))
>>> solver.check()
sat
>>> solver.model()
[reg_in_0 = 1, op_0 = 1, reg_out_0 = 1]

This is great: it prints sat, meaning that it found a solution, then showed the encoded values for the opcode and registers.

We'll write a helper function to make things human-readable:

def decode(prog, model):
    ''' Converts a program + solved model into SpringScript
    '''
    if len(model) == 0:
        return ' '
    ops = {0: 'AND', 1: 'OR', 2: 'NOT'}
    inputs = {i:c for (i,c) in enumerate('ABCDEFGHITJ')}
    outputs = {0: 'T', 1: 'J'}
    script = ''
    for (op, reg_in, reg_out) in prog:
        op = model.eval(op).as_long()
        reg_in = model.eval(reg_in).as_long()
        reg_out = model.eval(reg_out).as_long()

        op = ops.get(op, 'NOT')
        reg_in = inputs.get(reg_in, 'T')
        reg_out = outputs.get(reg_out, 'T')
        script += "%s %s %s\n" % (op, reg_in, reg_out)
    return script[:-1]

Running this on our solution, we see the resulting program:

>>> decode(prog, solver.model())
'OR B J'

This is an interesting solution: it actually ignores the hole, and uses the fact that sensor B is above a tile. Given the limited constraints which we provided, this is perfectly valid.

Bring me my 105 bits

Now, we can write our full solver, which takes a map string (e.g. ###..#..##) and asserts that the robot is airborn whenever it is above a hole:

def solve_for_map(m, length=15):
    (j, prog) = symbolic_execution(length)

    solver = Solver()
    jumps_at = []
    for (i,c) in enumerate(m):
        # We're in the air if we've jumped within 3 tiles
        airborn = Or(jumps_at[-3:])

        # If there's no tile underneath us, then we must be airborn
        if c != '#':
            solver.add(airborn)

        # Sensor readings are based on the upcoming map:
        sensors = {c: i + j + 1 >= len(m) or m[i + j + 1] == '#'
                   for (j,c) in enumerate('ABCDEFGHI')}

        # We jump if we're not airborn and the program says to jump
        jumps_at.append(And(Not(airborn), j(sensors)))

    r = solver.check()
    return decode(prog, solver.model()) if r == sat else False

Running this on a very simple map, we get a valid-but-unusual solution:

>>> print(solve_for_map('#####  #####'))
OR E T
NOT T J
OR J J
AND J T
AND T T
AND T T
AND T T
OR J T
OR T J
NOT T J
AND D T
OR B T
AND T T
NOT E J
NOT T J

Take a moment to think about this, and test it out in the simulator below:

Bring me... slightly fewer bits

Of course, this is because we asked for 15 instructions, so Z3 gave us 15 instructions. Many of them are nonsensical or have no effect, but the total behavior of the script matches our specification.

We can make the solutions tighter by solving for a minimal number of instructions. There's probably a clever way of doing this in Z3 itself, but I implemented it by just testing each program size, counting upwards:

def minimize_for_map(m):
    for i in range(0, 16):
        r = solve_for_map(m, i)
        if r:
            return r
    return False

Running this on our simple map, we find a hilarious one-instruction solution:

>>> minimize_for_map('#####  #####')
'NOT J J'

That's right: always be jumping.

Revisiting our map

Now, we can finally revisit the map from our problem input:

>>> print(minimize_for_map('##### ################ ## ############# #  ############# #### #  ######## ## ## # ######## # ##############  # ############# # ## ########### ## ##  #########   ##############  ## ## ####'))
OR H T
NOT C J
AND I T
OR T J
AND D J

This takes about three seconds on my laptop, finding a five-instruction solution.

Let's plug it in and see how it does:

It's worth taking a step back and recognizing that this is magical. In about 100 lines of Python, we've built a universal solver that pulls a SpringScript program out of thin air.

Caveat

This doesn't quite work for the Advent of Code bot simulator, which presents your bot with a series of smaller maps, rather than one long map.

To fix this, we can modify solve_for_map to take multiple inputs, i.e.

def solve_for_maps(maps, length=15):
    (j, prog) = symbolic_execution(length)
    solver = Solver()
    for m in maps:
        jumps_at = []
        for (i,c) in enumerate(m):
            # ...same as before...
    r = solver.check()
    return decode(prog, solver.model()) if r == sat else False

def minimize_for_maps(maps):
    for i in range(0, 16):
        # Call the multi-map function instead
        r = solve_for_maps(maps, i)
        if r:
            return r
    return False

Then pass it the full set of small maps:

>>> maps = ['#####.###########',
            '#####.##.########',
            '#####.#..########',
            '#####.####.#..###',
            '#####.##.##.#.###',
            '#####.#.#########',
            '#####..#.########',
            '#####.#.##.######',
            '#####.##.##..####',
            '#####...#########',
            '#####..##.##.####',
            '#####.#.###.#####',
            '#####.###.#..####',
            '#####...###...###',
            '#####.#.#.#.#.###']
>>> print(minimize_for_maps(maps))
NOT H J
OR C J
AND B J
AND A J
NOT J J
AND D J

This produces a slightly longer, six-instruction solution, which I believe to be minimal.

Upping the ante

Why are we given a whole 15 instructions?

Well, probably because humans aren't powerful boolean-crunching machines, so we're given some room for inefficiency.

This begs the question: what does a truly hard, adversarial map look like?

As it turns out, we can generate one with Z3!

Previously, we were evaluating over a symbolic program, but binding it to a particular set of sensor readings. Now, we take the next step into the Symbol-Verse and make the tiles in the map variables as well. Here's a modified version of solve_for_map which accepts tiles as variables, rather than a map string:

def solve_symbolic_map(m, length=15):
    ''' m is an array of BoolRef tiles, which may be variables
    '''
    (j, prog) = symbolic_execution(length)
    jumps_at = []
    conds = []
    for (i,t) in enumerate(m):
        # We're in the air if we've jumped within 3 tiles
        airborn = Or(jumps_at[-3:])

        # If there's no tile underneath us, then we must be airborn
        conds.append(Or(t, airborn))

        # Sensor readings are based on the upcoming map:
        sensors = {c: i + j + 1 >= len(m) or m[i + j + 1]
                   for (j,c) in enumerate('ABCDEFGHI')}

        # We jump if we're not airborn and the program says to jump
        jumps_at.append(And(Not(airborn), j(sensors)))

    return (prog, And(conds))

We can use this to solve for a matching map and program:

>>> m = [Bool('t_%i' % i) for i in range(5)]
>>> (p,c) = solve_symbolic_map(m, 1)
>>> solver = Solver()
>>> solver.add(c)
>>> solver.check(c)
sat
>>> model = solver.model()
>>> model
[t_0 = True,
 t_1 = True,
 t_4 = False,
 reg_in_0 = 0,
 t_2 = True,
 t_3 = True,
 reg_out_0 = 1,
 op_0 = 2]
>>> decode(p, model)
'NOT A J'
>>> ''.join(['#' if model.eval(t) else ' ' for t in m])
'#### '

This has produced a relatively boring map and a relatively boring program, but they're compatible!

How can we use this to generate hard maps?

We'll need to use a hithero-unused Z3 feature, qualifiers, to make an assertion of the form

This map can be solved with n instructions, but not with n - 1 instructions

This is translated into Z3 in a rather literal fashion:

>>> m = [Bool('t_%i' % i) for i in range(10)]
>>> s = Solver()
>>> (p, q) = solve_symbolic_map(m, 1)
>>> vars = sum(p, []) # flatten the list
>>> vars
[op_0, reg_in_0, reg_out_0]
>>> s.add(Not(Exists(vars, q))) # This is the tricky part!
>>> s.add(solve_symbolic_map(m, 2)[1])
>>> s.check()
sat
>>> model = s.model()
>>> ''.join(['#' if model.eval(t) else ' ' for t in m])
'###### #  '

Now we're getting somewhere! We've found a map which can't be solved in a single instruction:

>>> solve_for_map('###### #  ', 1)
False
>>> solve_for_map('###### #  ', 2)
'OR G J\nAND I J'

We could extend this to a huge map and let Z3 think for a while:

>>> m = [Bool('t_%i' % i) for i in range(100)]
>>> (p, q) = solve_symbolic_map(m, 14)
>>> s = Solver()
>>> vars = sum(p, [])
>>> s.add(Not(Exists(vars, q)))
>>> s.add(solve_symbolic_map(m, 15)[1])
>>> s.check()
# and now we wait...

In my rough testing, this takes approximately forever: existential qualifiers are a harder class of problem, and there are too many free variables.

It's easier to generate an adversarial map incrementally:

My implementation looks something like this:

m = [BoolVal(True)]
for instructions in range(2, 16):
    print("Solving for %i instructions" % instructions)
    while True:
        # Add 5 fresh boolean variables to the end of the map
        m += [Bool('t_%i' % (i + len(m))) for i in range(5)]
        print("   map size: %i" % len(m))

        s = Solver()
        (p, q) = solve_symbolic_map(m, instructions - 1)
        s.add(Not(Exists(sum(p, []), q)))
        s.add(solve_symbolic_map(m, instructions)[1])

        if s.check() == sat:
            model = s.model()
            # Update the map with the new tiles
            m = [BoolVal(bool(model.eval(i))) for i in m]

            q = ''.join('#' if i else ' ' for i in m)
            print("Found map '%s'" % q)
            break

Running this overnight on a friend's server, it finds a 131-tile map which can be solved in no fewer than 11 instructions:

(please don't try to solve this one by hand)

Generating an adversarial map which requires a full 15 instructions is probably out of my reach, but if anyone has clever ideas (or few thousand CPU-hours to spare), let me know!

Related work

This paper (and associated slides) talk about building a Z3 model for a full RISC-V CPU (!!).

If you like pulling things out of thin air, check out this blog post about using AFL to synthesize JPEGS.

ICFPC 2013 is a similar style of problem, and they also used Z3 to compare program equality.

Credits

Generating the adversarial map was made possible by Martin Galese; thanks for not questioning why I had a Python script using 100% of a CPU core on your workstation for days on end.

Pixel art is from the Kenney 1-Bit Pack.