This year was the 4th installment of Advent of Code and like the last years I focused on doing the puzzles in Haskell.

For the most part the puzzles where interesting and there where some gems in there that I had to research long forgotten algorithms again to get it done in reasonable time.

Then came day 23.

Problem description

I don't want to spoil too much so please go at the site and read the nice little story for yourself.

Basically you are given a list of about 1000 coordinates in 3D together with a radius. The coordinates are quite big and span a huge bounding box.

The first part (there are always two parts) is quite simple: you should just find the input with the largest radius and count all other nanobots (each input line is called a nanobot in the story) that are in range. Meaning the Manhatten-Distance between the strongest (biggest radius) bot and this other bot is less then the radius of our champion.

After parsing the input that's quite easy.

Then comes part 2 ... you are asked to find a coordinate that is in range of the most nanobots and if there are more than one position with the same amount of bots in range you should pick the one that is closer to the origin .

initial Solution

I have to admit: I had to think quite some time on this - the naive solution of trying each coordinate is practically impossible giving the huge bounding-box in 3D.

So thinking it's a cheap trick I tried only the given coords plus the vertices of the box given by these middle-points + the bots radius. Which would only meant checking around 9000 positions.

I think it even worked for the examples but of course it's wrong for the real input ... damn (btw: it's a nice task to figure out why this does not work, can you find a counter-example to this naive algorithm?)

Luckily I remembered an algorithm that is basically binary interval search in 3D - you start with the complete bounding box iteratively slice it into 8 half-size boxes always checking which one intersects the most bot-boxes.

This gives a quite fast solution and looks like this in Haskell (see Solution.hs for the complete solution):

But this post is not really about this solution.

people used what?

In this case I was quite proud (no I did get no points - never did, probably never will, those folks are insanely quick and I did not bother to wake up early to do this), and so I looked at reddit to see what other people did.

Indeed some used basically the same algorithm, some tried some greedy annealing like process (which I'm quite surprised worked) and then there where some who used SMT Solvers.

This really sparked my interest. And I finally found some time to play with it.

choosing a library/solver

I looked around a bit and it became quite clear that Z3 is a good choice as I wanted to try bindings with Haskell.

Initially I tried z3 Bindings for the Z3 Theorem Prover and after some confusion I got it working (turns out it only works with the 4.6.0 release, the Ubuntu repos only had 4.4 and I manually downloaded 4.8.x).

But this one does not seem to have bindings for the optimization part.

Next I looked at sbv and this one is a gem. Not only does it include everything for optimization, it also works with quite a lot of solvers and yes Z3 is the default and very easy to use.


I just downloaded the newest release from here, extracted the files somewhere and made a symbolic link to the binary (in ) into a folder that sits on my path.

That's it.

SBV calls the binary directly so that's enough - if you have something that needs to link to the libraries you probably have to add the includes and library paths to your build system (in Haskell/Stack this is done by adding entries to the ) or you can put the header files in and the libraries in this is where most linkers/compilers expect them to be on *nix.

using SBV

The rest was actually quite simple (you can find the complete file here).

SBV abstracts away many thinks and give you some monads to work in. Literals and Variables are instances of all the obvious calculation/math classes like , , ... so modelling is as simple as implementing it directly.

Just prepare to implement things like for yourself (maybe I missed it but I doubt that) the rest was easy for this case:

I'm no expert at all (indeed I'm a bloody noob) so maybe there are better ways but here I choose to define 3 variables and then the number of bots in range of these coordinate and, with lower priority - that's what the is for - the distance to the origin.

I only had to write the 3 helpers in the clause:

  • is a simple implementation of (checks if the variable given is bigger then 0, if so just returns the variable, if not the negated value - is SBV/Z3s version of ).
  • is calculating the Manhattan distance between the coordinate given by the variables and the fixed coordinates of a bot
  • is 1 if the variable is in range of the bot and 0 else. I had to annotated the to disambiguate types.


Well it works and prints

But it's a lot slower then the algorithm I showed above. I guess it's not that surprising (given the poor modeling I did) but I was almost expecting more from the way people scored with this.

I did not measure the time but it takes around 1 minute I think.

If anybody can give me some hints on how I can make this quicker with Z3 please leave me a message on Twitter or even better make a PR ;)


I like the approach and I will look more into Z3 in the future.

I think the next task will be to let it search for magic squares - my naive list-comprehension algorithm is OK for 4x4 squares but already fails at 5x5 and this solver should be able to get this quicker right?