This is a continuously updated post of my progress during Advent of Code 2021.

TLDR: I’m using Advent of Code as an opportunity to automate my problem solving skills

# Introduction

The Advent of Code is a yearly advent callender that presents you with interesting programming puzzles each day from December 1st up to Christmas. These problems are divided in two parts, where solving the first gives you access to the second. If you solve the first problem in the ‘right’ way, solving the second one won’t be much harder. Other days you find yourself rewriting everything from scratch. Making good puzzles is hard, so I’m very thankful for the people organizing it each year.

Last year I mainly used Python. For some challenges there was this great ‘aha’ moment when you can rephrase the problem in a different way that makes it much easier to solve. That was nice, but there was also this feeling of having to solve the same problems in the same ways as nearly every day in school or work; Write down the code that solves it and then iteratively replace data structures and algorithms to push down algorithmic complexity, which can start to feel repetitive sometimes and I quit the event halfway. This year I’ll try get more out of the challenges; hopefully by learning some skills or tools which can replace parts of the problem solving cycle

As a constraint for this year’s puzzles I’m giving myself the challenge to not write a single line of code that actually deals with solving the puzzles. Instead this has to be done via (modern) tools that solve the puzzles for me. See below for some examples of tools and methods that would be able to to this. Note that I’m looking at methods that I usually do not use, so if you are an expert you might not agree of my explanation of them :)

• Numerical solvers: Lots of problems can we represented in matrix form; think linear systems of equations or (integer) linear programming. For some probems there is an obvious translation, for others it might not be so obvious at first sight. Similarly some might have a natural expression as convex or general non-linear optimization problems. These usually have very thoroughly optimized solvers. I hardly ever make use of those tools, and should do so more often. Especially the part of recognizing and rephrasing non-trivial problems as matrix equations is a skill that I lack. Maybe using more math in general is a good idea.
• Symbolic solvers: Over the last few years I have become a fan of SymPy, an open source Computer Algebra System in Python. There are some unsolved bugs though, and after running into them I’ve started thinking about switching to diofant (a SymPy fork), at least for certain edge cases where SymPy fails. In short, with these tools you’ll get automatic differentiation and exact results where the numerical solvers only give estimates.
• Type directed code generation This is an area where I have absolutely no experience in. Back when I learned Haskell I thought that the ideal programming language would be one where you only write down function types and the language engine automatically infers the code for you. Later on I learned that there are some fundamental problems with that, but in more constrained environments people have figured out how to do this. For example some proof assistants have automatic proof search and within Haskell’s type system completely type guide code generation seems possible for simple types. This is a very active research area and I have yet to find a easy-to-use tool where we can put this to use, hopefully there is one (learning Coq or Agda looks painful). There also seems to be some progress by using both types and unit tests to specify the problem and interactively finding the solving code by cooperating with the code generator.
• Logic/query programming: Logic programming is another area where I have not gone further than the Getting_Started tutorials, but pretty sure there will be puzzles that are naturally expressed in Prolog. Related (relational?) might be straight up SQL, which I do have experience with. Using that would not teach me anything new, but it would fit the bill of giving a high-level problem description and letting the tool find the optimal way of solving it.
• SMT solvers: All NP problems (‘hard problems’) can be rewritten as as satisfiability problems. With the introduction of SMT solvers, algorithmic and computational advances and reasonable easy to use API’s we can use this property to solve interesting problems without having to specify the underlying algorithmic methods explicitly. The solver determines what kind of integers (bitvectors or unbounded) or even real numbers are allowed in the contraint expressions. Reading an article about improving the fast inverse square root constant using SMT solvers made me realize how powerful this method could be, but I never got around to putting in the effort of learning to use them beyond the ‘Hello world’ examples. Hopefully the Advent of Code will be good opportunity to learn more about it.
• Symbolic execution: Paired with both SMT solvers and symbolic solvers comes symbolic execution. In short, in this way you can translate code in your programming language of choice to SMT expressions by executing the code where some parameters are replaced by unknown named symbols. This is in particular powerful for problems that are naturally expressed as finding x in an equation f(x) = y for a given y and a complicated piece of code f containing branches or loops. One obvious use case is inverting machine code functions in crypto-challenges. For Python there is pySym and PyExZ3 which I both couldn’t get to work on my computer. One popular approach seems to compile code down to llvm and use that for symbolic execution.
• Direct solution via AI methods: Genetic programming might be useful for finding simple expressions in some cases and neural networks (or any other black box ML method) might be able to solve some problem given a lot of input-output examples. That last one does feel like cheating.
• AI code generation: Recent advances (and maybe an increase in ML researcher compute budgets) has created large language models that are able to infer code snippets based on natural language input. Some well known ones are OpenAI GPT-3, GitHub Copilot & SourceAI. One large difference to the previous methods is they are closed-source and currently only accesible via gated beta-programs. Until now I have only been admitted to OpenAI beta. Hopefully I’ll get through the Copilot & SourceAI waitlists as well. Altough I have been a little bit sceptical of these tools in the past, a quick test with copy-pasting last years challenges into OpenAI seemed very promising.

Of course there is some overlap between some of these methods, and the list is probably incomplete - so during the event there might be some new methods added. There will be 25 challenges, which means that each of these should at least be given a change once. Let’s get started!

# Day 1 : Letting OpenAI Davinci write some simple DSP code

Day one is a pretty simple puzzle. I thought it would be a good started for AI code generation as it is not dependant on code efficiency - it’s hard to write a solution that is not O(n). However, after trying out loads of different prompts I gave up on solving the challenge in one go. That just created very-close-but-just-not-correct solutions, like this one:

# You are an AI code assistant writing python code. Your task is to write a
# function in python that will take in a list of numbers. It should then
# count how many numbers are larger than the previous number in that list
# and return the count. The code is written here:

def count_occurence(numbers):
returns = 0
for number in numbers:
if number > previousNumber:
returns = returns + 1
print(returns)


which has a pretty obvious error. Note that I’m using the Davinci backend, not the Codex engine which should be much better at this task (still not accepted for beta). Maybe we should make it easier for the engine and break the problem up in two parts? We want to know how many differences are larger than zeros. Let’s start with the differences:

# This is a python function that given a list,
# returns the differences between successive
# numbers:

def diff(lst):
return [lst[i] - lst[i-1] for i in range(len(lst))]


… still not correct due to the off-by-one error, but we can (hackishly) solve that by adding 0 at the begin of the input list and subtracting 1 from the final answer. Then the second step:

# This is a python function that returns the
# count of numbers larger than 0 in a list:

def count_big(numbers):
count = 0
for i in range(len(numbers)):
if numbers[i] > 0:
count += 1
return count


That is a completely correct piece of code. We can then chain these as follows:

input = [int(x) for x in open('input/1_1.txt')] + [0]
print(-1 + count_big(diff(input)))


Which solves part one. Considering that the right answer was 1400 we could probably also have used a binary search…

For part 2, we ‘just’ have to add in another function to calculate the sums over the windows. Problem is, I could not convince Davinci to write a function that does that. Luckily there is another option. If we want to know whether two succesive window-of-three sums have a positive difference, we are essentially calculating $$x_i + x_{i+1} + x_{i+2} < x_{i+1} + x_{i+2} + x_{i+3}$$ which can be simplified to $$x_i < x_{i+3}$$. So we can rewrite the diff() function to look at larger offsets. Let’s try to convince the OpenAI engine:

# This is a python function that given a list of
# numbers and an index, iterates over the list
# and at each index i subtracts the item at i from
# the item at i - 3 and stores that in a new list:

def subtract_at(numbers, index):
new_list = []
for i in range(index, len(numbers)):
new_list.append(numbers[i] - numbers[i - 3])
return new_list


where only a very verbatim prompt seemed to work for generating the code. The index parameter in there is to remove the of-by-one errors Davinci often runs into (it was there in one of the earlier attempts and looked useful) So then the final solution is:

input = [int(x) for x in open('input/1_2.txt')]
diffs = subtract_at(input, 3)
print(count_big(diffs))


That completes day 1. Obviously, taking the AI code generation route made this puzzle much hard than it should have been. In part this is because I was using the wrong tool for the job - OpenAI Davinci is not made for these kind of things. In general, it seems like the AI could handle explicit ‘imperative’ prompts better than high level declarative codes. Also it got easily confused by off-by-one erros, just like human programmers. To solve that you can cheat by asking the engine to add an index parameter to your function, which I think is pretty funny. All 60 trial requests to the OpenAI API it took to write these 20 lines of code cost $0.94 of my free credits. To conclude, I’m pretty impressed with the abilities of Davinci to writing python code, but it seems more suited converting verbatim natural language to code than handing you the solution to a high level problem description (in this specific case at least). Looking at how well Github Copilot performed for others (just generating the code given the copy-pasted AoC description) suggests that OpenAI Codex would be much better suited for problem solving. # Day 2 : Submarine commands with the Lark parser generator Again, a pretty simple puzzle which made it hard to apply the more powerful methods mentioned in the introduction. After some thinking I settled on using a parser generator. At first Parsley looked like the right library to do this as it allows you to specify action within the grammar, but in the end I settled on lark as it handles left-recursion much better. So for part one that becomes: import collections from lark import Lark, Transformer, v_args Pos = collections.namedtuple('Pos', 'hor ver') @v_args(inline=True) class Submarine(Transformer): INT = int start = lambda : Pos(0, 0) forward = lambda pos, x: pos._replace(hor = pos.hor + x) down = lambda pos, x: pos._replace(ver = pos.ver + x) up = lambda pos, x: pos._replace(ver = pos.ver - x) parser = Lark(r''' ?start: course ?course: course "forward" INT "\n" -> forward | course "up" INT "\n" -> up | course "down" INT "\n" -> down | "\n" * -> start %ignore " " %import common.INT ''', parser='lalr', transformer=Submarine) with open('./input/2_1.txt') as f: pos = parser.parse(f.read()) print(pos.hor * pos.ver)  Looks pretty clean. For part two we need to modify the submarine to have an extra state variable aim. State = collections.namedtuple('Pos', 'hor ver aim') @v_args(inline=True) class SubmarinePart2(Transformer): INT = int start = lambda : State(0, 0, 0) forward = lambda state, x: state._replace(hor = state.hor + x, ver = state.ver + state.aim * x) down = lambda state, x: state._replace(aim = state.aim + x) up = lambda state, x: state._replace(aim = state.aim - x)  Conclusion: If you are parsing something that lookes like a dumbed down programming language, using a parser generator might make you life easier (altough it feels a bit overpowered in this case). Also, lark is nice. 4 stars, 46 to go. # Day 3 : Interactive programming with OpenAI Codex This one is too simple to solve using the advanced tools, but too hard for the AI code generator. So I broke my own rules and wrote down the solution for day 1: import numpy as np input = 1 * (np.array(open('./input/3_1.txt').read().splitlines(), dtype='c') == b'1') bits = np.arange(input.shape[1]-1, -1, -1) gam = ((input.mean(0) > .5) * 2**bits).sum() eps = ((input.mean(0) < .5) * 2**bits).sum() print(gam * eps)  Lets use OpenAI Davinci to ask for an explanation Explanation of what the code does: Input is a boolean array. The array is reshaped so it looks like the image (1 or 0). The mean of this image is calculated. A bitstring is created with each bit representing the mean over a certain range. The mean over that range is multiplied by 2**bits. 5 days later: I kind of gave up at this point because I didn’t know how to proceed. Solving part one this way felt like breaking the rules from the introduction and I didn’t want to continue doing that. Luckily I got accepted into the OpenAI Codex Beta today (yay!), which made part two easy to solve. The challenge was solved inside the OpenAI Playground, typing one command or function name at a time and then pressing Generate until I was happy. The code ended up being quite long, so it’s available as a gist for anyone interested. In short, here is a quick summary of my findings: • OpenAI Codex is much much smarter in writing code thatn OpenAI Davinci (as expected I guess) • But just pasting in the Advent of Code prompt did not work sadly • There was a hard to track bug in the final code - that boiled down to me not reading the problem description good enought (the equal numbers case) • I learned a new way to find the most common element in a list: max(set(x), key=x.count) • It’s very a good a generalizing patterns in the code. After having written the functions that deal with filtering on the most common bit, giving just one function name containing the word ‘least’ automatically lead to writing all the functions related to filtering on the least common bit. • I still had to break down the problem for the AI • In general it was a very nice experience and it felt like an actual helpful tool (no I’m not paid to write this) # Day 4 : Bingo with PySAT and Python-NNF So now I’m 5 days behind. Let’s rush through this. And play bingo apparently. Day 4 seems like a nice fit for trying out a SAT solver solver. It’s not a perfect match but I have never used one before so it will be a nice exercise. One way of using SAT solvers in python is using PySAT. PySAT expects expressions in ‘Conjunctive Normal Form’ (CNF), which is a bit hard for me to write directly. Luckily, some libraries like SymPy can also handle symbolic expressions containing booleans and have a nice to_cnf() function for performing the conversion for me. Hovewer, after some trial and error it was found that the Python-NNF library was much better suited for this task. In the conversion to CNF, SymPy gives itself the constraint not to introduce extra variables, while Python-NNF has no problems with that (as long as the satisfiability or the expression doesn’t change). SymPy therefore hangs for large expressions, while Python-NNF runs nearly instantly. Let’s start by reading in the board definition: def read_input(): boards = [] with open('./input/4_1.txt') as f: seq = next(f).split(',') try: while True: assert next(f) == '\n' boards.append([next(f).split() for _i in range(5)]) except StopIteration: return seq, boards seq, boards = read_input()  Now lets convert the boards to boolean expressions. from nnf import Var, And, Or def convert_board_to_boolean_expression(board): or_clauses = [] or_clauses.extend(And(map(Var, row)) for row in board) or_clauses.extend(And(map(Var, col)) for col in zip(*board)) return Or(or_clauses)  So we can transform a nice looking 5x5 board into a horrible expression that evaluates to true if any of the rows or columns in completely marked, like this:  (1 & 19 & 71 & 80 & 87) | (1 & 26 & 45 & 81 & 97) | (19 & 25 & 52 & 62 & 7) | (25 & 73 & 9 & 97 & 99) | (26 & 35 & 52 & 68 & 85) | (35 & 38 & 73 & 78 & 80) | (38 & 39 & 62 & 77 & 81) | (39 & 66 & 85 & 87 & 9) | (45 & 66 & 7 & 78 & 92) | (68 & 71 & 77 & 92 & 99)  Note how the variable names are numbers, which might be confusing but will make the final translation to PySAT readable CNF very easy. Also note our problem; this is perfect Disjunctive Normal Form (DNF) and not CNF. We also need to add in the contraint that we draw number from the bingo sequence in order: def convert_seq_to_boolean_expression(seq): return Or([And([Var(s, j <= i) for j, s in enumerate(seq)]) for i in range(len(seq))])  Which given the sequence [37,60,87] creates an expression like (37 & ~60 & ~87) | (37 & 60 & ~87) | (37 & 60 & 87)  Now we just need to Or() together all the boards and the sequenciality constraint and ask Python-NNF to convert that to CNF: expression = And([ convert_seq_to_boolean_expression(seq), Or(map(convert_board_to_boolean_expression, boards)) ]).to_CNF() print(expression.satisfiable()) # => prints True  Python-NNF also contains an interface against some SAT solvers, and is able to answer us that the expression is satisfiable and also which variables must be True or False. However, I will continue to use PySat for now as it also has support for weighted CNF formulas which are able to express the ‘first winner’ constraint - we do not just want any board that could win but the first board that wins. Beyond the formula that we want to have satified, we also add in some extra ‘soft’ clauses that have a weight that the solver tries to maximize. Let’s start constructing the formula: import collections from nnf import Aux from pysat.formula import WCNF # our expression will contain 'normal' variables like 24 and 50 # and auxilary variables like <a789>. The var_id dictionary will # convert both to PySAT indices free_vars = [v for v in expression.vars() if not isinstance(v, Aux)] safe_offset = int(max(free_vars, key=int)) + 2 - len(free_vars) var_id = collections.defaultdict(lambda: len(var_id) + safe_offset) for v in free_vars: var_id[v] = int(v) + 1 # add one because we can have 0 wcnf = WCNF() # Hard clauses: for or_clause in expression: # NNF negation (v.true = False) is a negative number in PySAT wcnf.append([var_id[v.name] if v.true else -var_id[v.name] for v in or_clause]) # Soft clauses: for n in seq: wcnf.append([-var_id[n]], weight=1)  Might be a bit harder to understand because of how PySAT uses integers to encode variables, but we now have our board game as a WCNF expression. Let’s solve it as a MaxSAT problem using RC2: from pysat.examples.rc2 import RC2 rc2 = RC2(wcnf) model = rc2.compute() print(rc2.cost) # prints 26 print([x-1 for x in model if x > 0 and x - 1 <= max(map(int, free_vars))]) # prints [6, 9, 13, 27, 30, 34, 37, 38, 40, 45, 49, 50, 54, 59, 60, 61, 63, 67, 72, 76, 82, 87, 88, 90, 97, 99]  Beautiful, that’s the minimum sequence that creates at least one winning board. Which board? Seems like I forgot to add a variable to track that. Let’s add some changes # Tag each board with an extra variable board_{index} expression = And([ convert_seq_to_boolean_expression(seq), Or([And([convert_board_to_boolean_expression(board), Var(f'board_{i}')]) for i, board in enumerate(boards)]) ]).to_CNF() # [..] # Add weighted claused to remove spurious board wins (could also use a am1 constraint I think) for k, v in var_id.items(): if str(k).startswith('board'): wcnf.append([-v], weight=1) # [...] # Handle board variables the same way as auxilary variables free_vars = [v for v in expression.vars() if not isinstance(v, Aux) and not v.startswith('board')] # [...] # Print out the winning board at the end board = [k for k, v in var_id.items() if v in model and str(k).startswith('board')] print(board) # prints ['board_14']  Now some some unreadble python to print out the winning board: winner = boards[int(board[0].split('_')[1])] print('\n'.join(''.join((f'<{cell}>' if int(cell) in sol else cell).center(10) for cell in row) for row in winner)) # <30> 93 48 17 33 # <67> 7 5 0 69 # <54> <76> 52 1 <87> # <99> 73 <50> 25 16 # <13> 20 41 77 62 sum_of_unmarked = sum(sum(int(cell) for cell in row if int(cell) not in sol) for row in winner) number_just_called = max(sol, key=lambda x: seq.index(str(x))) print(sum_of_unmarked * number_just_called)  Seems like we beat the bingo machine, on to part 2! So instead of finding out which board will win first, find out which board will win last. For one, that means replacing an Or() with and And(). expression = And([ convert_seq_to_boolean_expression(seq), And([And([convert_board_to_boolean_expression(board), Var(f'board_{i}')]) for i, board in enumerate(boards)]) ]).to_CNF() # [...] print('ndraws', len(sol))  which immediately gives the answer that that would take 86 draws. Problem is that we also need to know which board would be the last to win. Preferable, I’d like to answer that without modifiying the hard MaxSat equation, but I don’t think that that is possible. Iterating over the boards and checking which board is not satisfied after 85 seems to be a solution, altough I’d be happy to hear about better ways to handle this within a SAT solver. for board in boards: eq = convert_board_to_boolean_expression(board) if not eq.satisfied_by({ v: v in seq[:85] for v in eq.vars() }): winner = board print('\n'.join(''.join((f'<{cell}>' if cell in seq[:85] else cell).center(10) for cell in row) for row in winner)) sum_of_unmarked = sum(sum(int(cell) for cell in row if int(cell) not in sol) for row in winner) number_just_called = max(sol, key=lambda x: seq.index(str(x))) print(sum_of_unmarked * number_just_called)  which also prints out a beautiful just not solved board:  93 <7> <60> <75> <12> <49> <64> 20 <46> <10> <3> <23> <76> 42 <47> <9> 22 <6> <34> <87> <41> <37> <66> <45> 48  # Day 5 : Hydrothermal vents (cheating) Draw horizontal & vertical lines, find points where they overlap. That’s a pretty easy puzzle and as I’m still 4 days behind I’ll just cheat my way through part 1: import collections import re import numpy as np hits = collections.Counter() for line in open('./input/5.txt'): x1, y1, x2, y2 = map(int, re.match(r'^(\d+),(\d+) -> (\d+),(\d+)\n$', line).groups())
if x1 == x2 or y1 == y2:
x1, x2 = sorted([x1, x2])
y1, y2 = sorted([y1, y2])
for x in range(x1, x2+1):
for y in range(y1, y2+1):
hits[x, y] += 1

print(sum(v > 1 for v in hits.values()))


For part 2 we add in another if statement:

elif abs(x2 - x1) == abs(y2 - y1):
for i in range(abs(x2-x1)+1):
x = x1 + i*np.sign(x2-x1)
y = y1 + i*np.sign(y2-y1)
hits[x, y] += 1


Only 3 days behind now :)

# Day 6 : Linear algebra

Exponential growth rates - this should be doable with one of the scientific tools

• each lanternfish creates a new lanternfish once every 7 days
• new lanternfish: two more days for its first cycle.

So that’s 7 counters to model the normal lanternfishes, and 2 more for the newly spawned ones. Matrix multiplication is a pretty obvious solution, but scrolling through hacker news I already found a matrix solution to it a few days ago. So let’s think of different options.

Nope. Let’s just go with a matrix product. I feel stupid for reading that article, now it feels like I’m stealing an idea. Here is the code to construct the matrix:

import numpy as np

def state_next(state):
(day0, day1, day2,
day3, day4, day5,
day6, day7, day8) = state
return np.array([
day1, day2, day3,
day4, day5, day6,
day0+day7, day8, day0
])

transition_matrix = state_next(np.eye(9, dtype='int64'))
print(transition_matrix)

# [[0 1 0 0 0 0 0 0 0]
#  [0 0 1 0 0 0 0 0 0]
#  [0 0 0 1 0 0 0 0 0]
#  [0 0 0 0 1 0 0 0 0]
#  [0 0 0 0 0 1 0 0 0]
#  [0 0 0 0 0 0 1 0 0]
#  [1 0 0 0 0 0 0 1 0]
#  [0 0 0 0 0 0 0 0 1]
#  [1 0 0 0 0 0 0 0 0]]


Then, to calculate what happens with the initial state in the day 1 example, we can derive a vector that automatically steps through 18 days of simulation and then sums everything together:

fish_after_18_days = np.linalg.matrix_power(transition_matrix, 18).sum(0)

(day0, day1, day2,
day3, day4, day5,
day6, day7, day8) = np.eye(9, dtype='int64')

init = day3 + day4 + day3 + day1 + day2

print( fish_after_18_days @ init ) # => should print 26


To solve it for the real challenge:

input = open('input/6.txt').read().rstrip().split(',')
init = sum(input.count(str(i))*one_hot for i, one_hot in enumerate(np.eye(9, dtype='int64')))
fish_after_80_days = np.linalg.matrix_power(transition_matrix, 80).sum(0)
print(fish_after_80_days @ init)


Yep that’s it. For part two we are interested in what happens after 256 days. Luckily the answer fits in a 64 bit integer so typing up this sentence took longer than solving part 2. On to day 7, just two more days until I’m on par again.

# Day 7 : SciPy Simplicial Homology Global Optimization

We’re getting hunted by a whale and crabs in submarines are going to rescue us by blasting a hole in the ocean floor to open up a underground case system. Interesting :O

To do that, we’ll need to horizontally align the submarines while making them move as little as possible. Sounds like an optimization problem.

import numpy as np
from scipy.optimize import shgo

def loss(target_pos):
return abs(hor_pos - target_pos).sum()

bounds = [(hor_pos.min(), hor_pos.max())]
optimal_target = round(shgo(loss, bounds).x.item())
print(loss(optimal_target))


scipy.optimize.minimize also gives the right answer but global optimization might be more correct here.

For part two we can just update the loss function:

def loss(target_pos):
d = abs(hor_pos - target_pos)
return (d * (d + 1) / 2).sum()


Both loss functions look convex when plotted using matplotlib so that’s probably the reason the actual solver doesn’t matter too much.

Just one more day and I’m not running behind anymore

# Day 8 : Z3

The background story for the puzzle suggests we will be able to use some really interesting SAT solver techniques. Except the first puzzle ended up being rather easy:

import numpy as np

lines = list(open('input/8.txt'))

output_lengths = [
len(digit)
for line in lines
for digit in line.split(' | ')[1].split()]

print(
output_lengths.count(2) + # digit 1
output_lengths.count(4) + # digit 4
output_lengths.count(3) + # digit 7
output_lengths.count(7)   # digit 8
)


So let’s hope part 2 is a bit more interesting. And it is! I guess I get to use an SMT solver here (it must be doable with a SAT solver but SMT will make things much easier here because you don’t have to deal with normalization forms).

(Quite some time later)..

Yep Z3 python is great and was able to solve it. I really did not have to think about the actual problem solving implementation. The bad part is that it took over 3 minutes to compute the final answer. Strange how waiting 3 minutes for a computation that saves you maybe half an hour of thinking feels bad :) The code is over here. In short, we encode the constraints that all digits are used exactly once in the signal patterns (using PbEq) and then we add clauses that a certain pattern being a certain digit Implies() that exactly one of all the possible permutations of the pattern mapping to actual digit segments must be true. That last part is the slow part as permutations of larger segment counts become very sizable. But it works, and it was the first time I actually got to use an SMT solver. Now I’m finally on par with the advent of code again. Looking forward to day 9!

# Day 9: NetworkX Connected Components

Challenge one was: given a 2 dimensional heightmap of integers, find the points with all neighbours at a larger elevation.

import numpy as np

h = np.array(input, dtype='c').astype(int)

pits = ((h < nn[2:  ,1:-1]) &
(h < nn[ :-2,1:-1]) &
(h < nn[1:-1,2:  ]) &
(h < nn[1:-1, :-2]))

print((h[pits] + 1).sum())


Then the second part was finding the sizes of the largest three basins, all basins being separated by the number 9. This one is a bit tougher, but I settled on using a graph theoretical method because I hadn’t used that before for AoC. In short, we construct a ‘grid graph’ where each node corresponds to a point on the heightmap. Then we remove all the barrier points from that graph and ask NetworkX to calculate the connected components. Then we sort that list based on connected components size and pick the largest three.

import numpy as np, networkx as nx


Note the nodes variable. It might look a bit confusing, but it just constructs an 100x100x2 array where each (i,j) point is (i,j) - the name of that point in the networkx grid array. That was the first time I got to use np.mgrid as well which has a pretty nice syntax.