Or How Much is ever Enough?

This year, I am having fun taking part in my first ever Advent of Code! Day 17 threw me for a loop and forced me to learn a new technique so that deserves a quick write-up. As with other days, it’s a two part challenge which starts easy. The first challenge involves a bytecode interpreter and you know how much I like those! My input is equivalent to the following Python code:

So far so good. Part 2 gets hairy and involves searching for the smallest argument a that turns the device into a quine. Simplifying the program as shown below highlights the fact that device yields one value per octal digit of a. So we’re looking for an a with 16 octal digits. There are \(2^{48}\) of those! This reminds us of the wheat and chessboard problem and we quickly realize that a brute-force search will run into heat death of the universe issues (although not quite as quickly as I would like to admit). The two editors share an interpreter, so run the one above first:

I could vaguely remember reading something about SAT solvers and Bit Twiddling Hacks. The combined search took me to this page and the following Z3-based solution:

Z3 solves this problem so fast, its runtime is barely noticeable. That’s impressive on several levels:

  • pip install z3-solver just worked™
  • the API is n00b-friendly
  • solution is accepted by AoC

In my defense, I had worked with algebraic modeling languages before but Z3 remains an impressive bit of tech.

Still, I couldn’t help but feel that I brought a gun to a knife fight. (Don’t get me wrong, I absolutely took the AoC credit but I didn’t love the black box solution). So I stared at the short implementation for a while longer and found an alternative solution. It’s plain enough that MicroPython runs it too, without Pyodide’s heavier download:

Ultimately, this amounts to backward induction which is likely one of the many strategies that Z3 implements. Unlike the brute-force approach, this implementation prunes aggressively which keeps its complexity manageable.